// © 2019, ETH Zurich
//
// This Source Code Form is subject to the terms of the Mozilla Public
// License, v. 2.0. If a copy of the MPL was not distributed with this
// file, You can obtain one at http://mozilla.org/MPL/2.0/.

use super::{
    counterexamples::DiscriminantsStateInterface, high::generics::HighGenericsEncoderInterface,
};
use crate::{
    encoder::{
        builtin_encoder::BuiltinMethodKind,
        errors::{
            error_manager::PanicCause, EncodingError, EncodingErrorKind, EncodingResult, ErrorCtxt,
            SpannedEncodingError, SpannedEncodingResult, WithSpan,
        },
        foldunfold,
        high::types::HighTypeEncoderInterface,
        initialisation::InitInfo,
        loop_encoder::{LoopEncoder, LoopEncoderError},
        mir::{
            contracts::{ContractsEncoderInterface, ProcedureContract},
            procedures::encoder::specification_blocks::SpecificationBlocks,
            pure::{PureFunctionEncoderInterface, SpecificationEncoderInterface},
            sequences::MirSequencesEncoderInterface,
            spans::interface::SpanInterface,
            specifications::SpecificationsInterface,
            type_invariants::TypeInvariantEncoderInterface,
            types::MirTypeEncoderInterface,
        },
        mir_encoder::{
            ExprOrArrayBase, FakeMirEncoder, MirEncoder, PlaceEncoder, PlaceEncoding,
            PRECONDITION_LABEL,
        },
        mir_successor::MirSuccessor,
        places::{Local, LocalVariableManager, Place},
        snapshot::interface::SnapshotEncoderInterface,
        Encoder,
    },
    error_unsupported,
    utils::is_reference,
};
use ::log::{debug, trace};
use prusti_common::{
    config,
    utils::to_string::ToString,
    vir::{fixes::fix_ghost_vars, ToGraphViz},
    vir_expr, vir_local, vir_stmt,
};
use prusti_interface::{
    data::ProcedureDefId,
    environment::{
        borrowck::{facts, regions::PlaceRegionsError},
        mir_utils::SliceOrArrayRef,
        polonius_info::{
            LoanPlaces, PoloniusInfo, PoloniusInfoError, ReborrowingDAG, ReborrowingDAGNode,
            ReborrowingKind, ReborrowingZombity,
        },
        BasicBlockIndex, LoopAnalysisError, PermissionKind, Procedure,
    },
    specs::{
        typed,
        typed::{Pledge, SpecificationItem},
    },
    utils, PrustiError,
};
use prusti_rustc_interface::{
    errors::MultiSpan,
    index::IndexSlice,
    middle::{
        mir,
        mir::{Mutability, TerminatorKind},
        ty::{self, GenericArgsRef},
    },
    span::Span,
    target::abi::{FieldIdx, Integer},
};
use rustc_hash::{FxHashMap, FxHashSet};
use std::{
    collections::BTreeMap,
    convert::TryInto,
    fmt::{Debug, Write},
};
use vir_crate::polymorphic::{
    self as vir, borrows::Borrow, collect_assigned_vars, compute_identifier, CfgBlockIndex,
    ExprIterator, Float, Successor, Type,
};

pub struct ProcedureEncoder<'p, 'v: 'p, 'tcx: 'v> {
    encoder: &'p Encoder<'v, 'tcx>,
    proc_def_id: ProcedureDefId,
    procedure: &'p Procedure<'tcx>,
    mir: &'p mir::Body<'tcx>,
    specification_blocks: SpecificationBlocks,
    specification_block_encoding: BTreeMap<mir::BasicBlock, Vec<vir::Stmt>>,
    cfg_method: vir::CfgMethod,
    locals: LocalVariableManager<'tcx>,
    loop_encoder: LoopEncoder<'p, 'tcx>,
    auxiliary_local_vars: FxHashMap<String, vir::Type>,
    mir_encoder: MirEncoder<'p, 'v, 'tcx>,
    check_panics: bool,
    check_foldunfold_state: bool,
    polonius_info: Option<PoloniusInfo<'p, 'tcx>>,
    procedure_contract: Option<ProcedureContract<'tcx>>,
    label_after_location: FxHashMap<mir::Location, String>,
    /// Store the CFG blocks that encode a MIR block each.
    cfg_blocks_map: FxHashMap<mir::BasicBlock, FxHashSet<CfgBlockIndex>>,
    /// Contains the boolean local variables that became `true` the first time the block is executed
    cfg_block_has_been_executed: FxHashMap<mir::BasicBlock, vir::LocalVar>,
    /// Magic wand generated by a call at a given location with a label used in post.
    magic_wand_at_location: FxHashMap<mir::Location, (String, vir::Expr, vir::Expr)>,
    /// Magic wand components from array accesses at a location:
    ///  - resolved value field for the wand LHS (LHS is always a single variable)
    ///  - regained array variable
    ///  - info about updated and restored array elements
    array_magic_wand_at: FxHashMap<mir::Location, (vir::Expr, vir::Expr, vir::Expr)>,
    /// Labels for array equalities in loops
    array_loop_old_label: FxHashMap<BasicBlockIndex, String>,
    /// Slices created at certain locations
    slice_created_at: FxHashMap<mir::Location, vir::Expr>,
    // /// Contracts of functions called at given locations with map for replacing fake expressions.
    procedure_contracts:
        FxHashMap<mir::Location, (ProcedureContract<'tcx>, FxHashMap<vir::Expr, vir::Expr>)>,
    /// A map that stores local variables used to preserve the value of a place accross the loop
    /// when we cannot do that by using permissions.
    pure_var_for_preserving_value_map:
        FxHashMap<BasicBlockIndex, FxHashMap<vir::Expr, vir::LocalVar>>,
    /// Information about which places are definitely initialised.
    init_info: InitInfo,
    /// Mapping from old expressions to ghost variables with which they were replaced.
    old_to_ghost_var: FxHashMap<vir::Expr, vir::Expr>,
    /// Ghost variables used inside package statements.
    old_ghost_vars: FxHashMap<String, vir::Type>,
    /// For each loop head, the block at whose end the loop invariant holds
    cached_loop_invariant_block: FxHashMap<BasicBlockIndex, BasicBlockIndex>,
    /// Type substitutions inside this procedure. Most likely identity for the
    /// given proc_def_id.
    substs: GenericArgsRef<'tcx>,
}

impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
    #[tracing::instrument(name = "ProcedureEncoder::new", level = "debug", skip_all, fields(proc_def_id = ?procedure.get_id()))]
    pub fn new(
        encoder: &'p Encoder<'v, 'tcx>,
        procedure: &'p Procedure<'tcx>,
    ) -> SpannedEncodingResult<Self> {
        let mir = procedure.get_mir();
        let proc_def_id = procedure.get_id();
        let substs = encoder.env().query.identity_substs(proc_def_id);
        let tcx = encoder.env().tcx();
        let mir_encoder = MirEncoder::new(encoder, mir, proc_def_id);
        let init_info = InitInfo::new(mir, tcx, proc_def_id, &mir_encoder)
            .with_default_span(procedure.get_span())?;

        let specification_blocks =
            SpecificationBlocks::build(encoder.env().query, mir, procedure, false);

        let cfg_method = vir::CfgMethod::new(
            // method name
            encoder.encode_item_name(proc_def_id),
            // formal returns
            vec![],
            // local vars
            vec![],
            // reserved labels
            vec![],
        );

        Ok(ProcedureEncoder {
            encoder,
            proc_def_id,
            procedure,
            mir,
            cfg_method,
            specification_blocks,
            specification_block_encoding: Default::default(),
            locals: LocalVariableManager::new(&mir.local_decls),
            loop_encoder: LoopEncoder::new(procedure, tcx),
            auxiliary_local_vars: FxHashMap::default(),
            mir_encoder,
            check_panics: config::check_panics(),
            check_foldunfold_state: config::check_foldunfold_state(),
            polonius_info: None,
            procedure_contract: None,
            label_after_location: FxHashMap::default(),
            cfg_block_has_been_executed: FxHashMap::default(),
            cfg_blocks_map: FxHashMap::default(),
            magic_wand_at_location: FxHashMap::default(),
            array_magic_wand_at: FxHashMap::default(),
            array_loop_old_label: FxHashMap::default(),
            slice_created_at: FxHashMap::default(),
            procedure_contracts: FxHashMap::default(),
            pure_var_for_preserving_value_map: FxHashMap::default(),
            init_info,
            old_to_ghost_var: FxHashMap::default(),
            old_ghost_vars: FxHashMap::default(),
            cached_loop_invariant_block: FxHashMap::default(),
            substs,
        })
    }

    #[tracing::instrument(level = "trace", skip_all)]
    fn encode_specification_blocks(&mut self) -> SpannedEncodingResult<()> {
        // Collect the entry points into the specification blocks.
        let mut entry_points: BTreeMap<_, _> = self
            .specification_blocks
            .entry_points()
            .map(|bb| (bb, Vec::new()))
            .collect();

        // Encode the specification blocks.
        for (bb, statements) in &mut entry_points {
            self.encode_specification_block(*bb, statements)?;
        }
        assert!(self.specification_block_encoding.is_empty());
        self.specification_block_encoding = entry_points;

        Ok(())
    }

    #[allow(clippy::nonminimal_bool)]
    fn encode_specification_block(
        &mut self,
        bb: mir::BasicBlock,
        encoded_statements: &mut Vec<vir::Stmt>,
    ) -> SpannedEncodingResult<()> {
        let block = &self.mir[bb];
        let _ = self.try_encode_assert(bb, block, encoded_statements)?
            || self.try_encode_assume(bb, block, encoded_statements)?
            || self.try_encode_refute(bb, block, encoded_statements)?;
        Ok(())
    }

    fn try_encode_assume(
        &mut self,
        bb: mir::BasicBlock,
        block: &mir::BasicBlockData<'tcx>,
        encoded_statements: &mut Vec<vir::Stmt>,
    ) -> SpannedEncodingResult<bool> {
        for stmt in &block.statements {
            if let mir::StatementKind::Assign(box (
                _,
                mir::Rvalue::Aggregate(box mir::AggregateKind::Closure(cl_def_id, cl_substs), _),
            )) = stmt.kind
            {
                if self.encoder.get_prusti_assumption(cl_def_id).is_none() {
                    return Ok(false);
                }
                let assume_expr = self.encoder.encode_invariant(
                    self.mir,
                    bb,
                    self.proc_def_id,
                    cl_substs,
                    false,
                )?;

                let assume_stmt = vir::Stmt::Inhale(vir::Inhale { expr: assume_expr });

                encoded_statements.push(assume_stmt);

                return Ok(true);
            }
        }
        Ok(false)
    }

    fn try_encode_assert(
        &mut self,
        bb: mir::BasicBlock,
        block: &mir::BasicBlockData<'tcx>,
        encoded_statements: &mut Vec<vir::Stmt>,
    ) -> SpannedEncodingResult<bool> {
        for stmt in &block.statements {
            if let mir::StatementKind::Assign(box (
                _,
                mir::Rvalue::Aggregate(box mir::AggregateKind::Closure(cl_def_id, cl_substs), _),
            )) = stmt.kind
            {
                let assertion = match self.encoder.get_prusti_assertion(cl_def_id) {
                    Some(spec) => spec,
                    None => return Ok(false),
                };

                let span = self
                    .encoder
                    .get_definition_span(assertion.assertion.to_def_id());

                let assert_expr = self.encoder.encode_invariant(
                    self.mir,
                    bb,
                    self.proc_def_id,
                    cl_substs,
                    false,
                )?;

                let assert_stmt = vir::Stmt::Assert(vir::Assert {
                    expr: assert_expr,
                    position: self.register_error(span, ErrorCtxt::Panic(PanicCause::Assert)),
                });

                encoded_statements.push(assert_stmt);

                return Ok(true);
            }
        }
        Ok(false)
    }

    fn try_encode_refute(
        &mut self,
        bb: mir::BasicBlock,
        block: &mir::BasicBlockData<'tcx>,
        encoded_statements: &mut Vec<vir::Stmt>,
    ) -> SpannedEncodingResult<bool> {
        for stmt in &block.statements {
            if let mir::StatementKind::Assign(box (
                _,
                mir::Rvalue::Aggregate(box mir::AggregateKind::Closure(cl_def_id, cl_substs), _),
            )) = stmt.kind
            {
                let refutation = match self.encoder.get_prusti_refutation(cl_def_id) {
                    Some(spec) => spec,
                    None => return Ok(false),
                };

                let span = self
                    .encoder
                    .get_definition_span(refutation.refutation.to_def_id());

                let refute_expr = self.encoder.encode_invariant(
                    self.mir,
                    bb,
                    self.proc_def_id,
                    cl_substs,
                    false,
                )?;

                let refute_stmt = vir::Stmt::Refute(vir::Refute {
                    expr: refute_expr,
                    position: self.register_error(span, ErrorCtxt::Panic(PanicCause::Refute)),
                });

                encoded_statements.push(refute_stmt);

                return Ok(true);
            }
        }
        Ok(false)
    }

    fn translate_polonius_error(&self, error: PoloniusInfoError) -> SpannedEncodingError {
        match error {
            PoloniusInfoError::UnsupportedLoanInLoop {
                loop_head,
                variable,
            } => {
                let msg = if self.mir.local_decls[variable].is_user_variable() {
                    "creation of loan 'FIXME: extract variable name' in loop is unsupported"
                        .to_string()
                } else {
                    "creation of temporary loan in loop is unsupported".to_string()
                };
                SpannedEncodingError::unsupported(
                    msg,
                    self.mir_encoder.get_span_of_basic_block(loop_head),
                )
            }

            PoloniusInfoError::LoansInNestedLoops(location1, _loop1, _location2, _loop2) => {
                SpannedEncodingError::unsupported(
                    "creation of loans in nested loops is not supported".to_string(),
                    self.mir.source_info(location1).span,
                )
            }

            PoloniusInfoError::ReborrowingDagHasNoMagicWands(location) => {
                SpannedEncodingError::unsupported(
                    "the creation of loans in this loop is not supported \
                    (ReborrowingDagHasNoMagicWands)",
                    self.mir.source_info(location).span,
                )
            }

            PoloniusInfoError::MultipleMagicWandsPerLoop(location) => {
                SpannedEncodingError::unsupported(
                    "the creation of loans in this loop is not supported \
                    (MultipleMagicWandsPerLoop)",
                    self.mir.source_info(location).span,
                )
            }

            PoloniusInfoError::MagicWandHasNoRepresentativeLoan(location) => {
                SpannedEncodingError::unsupported(
                    "the creation of loans in this loop is not supported \
                    (MagicWandHasNoRepresentativeLoan)",
                    self.mir.source_info(location).span,
                )
            }

            PoloniusInfoError::PlaceRegionsError(PlaceRegionsError::Unsupported(msg), span) => {
                SpannedEncodingError::unsupported(msg, span)
            }

            PoloniusInfoError::LoanInUnsupportedStatement(msg, location) => {
                SpannedEncodingError::unsupported(msg, self.mir.source_info(location).span)
            }
        }
    }

    fn polonius_info(&self) -> &PoloniusInfo<'p, 'tcx> {
        self.polonius_info.as_ref().unwrap()
    }

    fn procedure_contract(&self) -> &ProcedureContract<'tcx> {
        self.procedure_contract.as_ref().unwrap()
    }

    #[tracing::instrument(level = "debug", skip(self), fields(name = self.cfg_method.name()))]
    pub fn encode(mut self) -> SpannedEncodingResult<vir::CfgMethod> {
        let mir_span = self.mir.span;

        // Retrieve the contract
        let procedure_contract = self
            .encoder
            .get_procedure_contract_for_def(self.proc_def_id, self.substs)
            .with_span(mir_span)?;
        assert_one_magic_wand(procedure_contract.borrow_infos.len()).with_span(mir_span)?;
        self.procedure_contract = Some(procedure_contract);

        // Declare the formal return
        for local in self.mir.local_decls.indices().take(1) {
            let name = self.mir_encoder.encode_local_var_name(local);
            let typ = self
                .encoder
                .encode_type(self.mir_encoder.get_local_ty(local))
                .unwrap(); // will panic if attempting to encode unsupported type
            self.cfg_method.add_formal_return(&name, typ)
        }

        // Preprocess loops
        for bbi in self.procedure.get_reachable_nonspec_cfg_blocks() {
            if self.loop_encoder.loops().is_loop_head(bbi) {
                match self.loop_encoder.get_loop_invariant_block(bbi) {
                    Err(LoopEncoderError::LoopInvariantInBranch(loop_head)) => {
                        return Err(SpannedEncodingError::incorrect(
                            "the loop invariant cannot be in a conditional branch of the loop",
                            self.get_loop_span(loop_head),
                        ));
                    }
                    Ok(loop_inv_bbi) => {
                        self.cached_loop_invariant_block.insert(bbi, loop_inv_bbi);
                    }
                }
            }
        }

        // Load Polonius info
        self.polonius_info = Some(
            PoloniusInfo::new(
                self.encoder.env(),
                self.procedure,
                &self.cached_loop_invariant_block,
            )
            .map_err(|err| self.translate_polonius_error(err))?,
        );

        // Initialize CFG blocks
        let start_cfg_block = self.cfg_method.add_block(
            "start",
            vec![
                vir::Stmt::comment("========== start =========="),
                // vir::Stmt::comment(format!("Name: {:?}", self.procedure.get_name())),
                vir::Stmt::comment(format!("Def path: {:?}", self.procedure.get_def_path())),
                vir::Stmt::comment(format!("Span: {:?}", self.procedure.get_span())),
            ],
        );

        let return_cfg_block = self.cfg_method.add_block(
            "return",
            vec![
                vir::Stmt::comment("========== return =========="),
                vir::Stmt::comment("Target of any 'return' statement."),
            ],
        );
        self.cfg_method
            .set_successor(return_cfg_block, Successor::Return);

        // Encode a flag that becomes true the first time a block is executed
        for bbi in self.procedure.get_reachable_nonspec_cfg_blocks() {
            let executed_flag_var = self.cfg_method.add_fresh_local_var(vir::Type::Bool);
            let bb_pos = self
                .mir_encoder
                .register_span(self.mir_encoder.get_span_of_basic_block(bbi));
            self.cfg_method.add_stmt(
                start_cfg_block,
                vir::Stmt::Assign(vir::Assign {
                    target: vir::Expr::local(executed_flag_var.clone()).set_pos(bb_pos),
                    source: false.into(),
                    kind: vir::AssignKind::Copy,
                }),
            );
            self.cfg_block_has_been_executed
                .insert(bbi, executed_flag_var);
        }

        self.encode_specification_blocks()?;

        // Encode all blocks
        let (opt_body_head, unresolved_edges) = self.encode_blocks_group(
            "",
            &self.procedure.get_reachable_nonspec_cfg_blocks(),
            0,
            return_cfg_block,
        )?;
        if !unresolved_edges.is_empty() {
            return Err(SpannedEncodingError::internal(
                format!("there are unresolved CFG edges in the encoding: {unresolved_edges:?}"),
                mir_span,
            ));
        }

        // Set the first CFG block
        self.cfg_method.set_successor(
            start_cfg_block,
            Successor::Goto(opt_body_head.unwrap_or(return_cfg_block)),
        );

        // Prepare assertions to check specification refinement
        let (precondition_weakening, postcondition_strengthening) =
            self.encode_spec_refinement(PRECONDITION_LABEL)?;

        // Encode preconditions
        self.encode_preconditions(start_cfg_block, precondition_weakening)?;

        // Encode postcondition
        self.encode_postconditions(return_cfg_block, postcondition_strengthening)?;

        let local_vars: Vec<_> = self
            .locals
            .iter()
            .filter(|local| !self.locals.is_return(*local))
            .collect();
        for local in local_vars.iter() {
            let local_ty = self.locals.get_type(*local);
            let typ = self.encoder.encode_type(local_ty).unwrap(); // will panic if attempting to encode unsupported type
            let var_name = self.locals.get_name(*local);
            self.cfg_method.add_local_var(&var_name, typ);
        }

        self.check_vir()?;
        let method_name = self.cfg_method.name();
        let source_filename = self.encoder.env().name.source_file_name();

        self.encoder
            .log_vir_program_before_foldunfold(self.cfg_method.to_string());

        // Dump initial CFG
        if config::dump_debug_info() {
            prusti_common::report::log::report_with_writer(
                "graphviz_method_before_foldunfold",
                format!("{source_filename}.{method_name}.dot"),
                |writer| self.cfg_method.to_graphviz(writer),
            );
        }

        // Patch snapshots
        self.cfg_method = self
            .encoder
            .patch_snapshots_method(self.cfg_method)
            .with_span(mir_span)?;

        // Add fold/unfold
        let loan_locations = self
            .polonius_info()
            .loan_locations()
            .iter()
            .map(|(loan, location)| (loan.index().into(), *location))
            .collect();
        let method_pos = self.register_error(self.mir.span, ErrorCtxt::Unexpected);
        let method_with_fold_unfold = foldunfold::add_fold_unfold(
            self.encoder,
            self.cfg_method,
            &loan_locations,
            &self.cfg_blocks_map,
            method_pos,
        )
        .map_err(|foldunfold_error| match foldunfold_error {
            foldunfold::FoldUnfoldError::Unsupported(msg) => {
                SpannedEncodingError::unsupported(msg, mir_span)
            }

            _ => SpannedEncodingError::internal(
                format!("cannot generate fold-unfold Viper statements. {foldunfold_error}",),
                mir_span,
            ),
        })?;

        // Fix variable declarations.
        let method_with_fold_unfold = fix_ghost_vars(method_with_fold_unfold);

        // Dump final CFG
        if config::dump_debug_info() {
            prusti_common::report::log::report_with_writer(
                "graphviz_method_before_viper",
                format!("{source_filename}.{method_name}.dot"),
                |writer| method_with_fold_unfold.to_graphviz(writer),
            );
        }

        Ok(method_with_fold_unfold)
    }

    /// Encodes a topologically ordered group of blocks.
    ///
    /// Returns:
    /// * The first CFG block of the encoding.
    /// * A vector of unresolved edges.
    #[allow(clippy::type_complexity)]
    #[tracing::instrument(level = "debug", skip_all)]
    fn encode_blocks_group(
        &mut self,
        label_prefix: &str,
        ordered_group_blocks: &[BasicBlockIndex],
        group_loop_depth: usize,
        return_block: CfgBlockIndex,
    ) -> SpannedEncodingResult<(Option<CfgBlockIndex>, Vec<(CfgBlockIndex, BasicBlockIndex)>)> {
        // Encode the CFG blocks
        let mut bb_map: FxHashMap<_, _> = FxHashMap::default();
        let mut unresolved_edges: Vec<_> = vec![];
        for &curr_bb in ordered_group_blocks.iter() {
            let loop_info = self.loop_encoder.loops();
            let curr_loop_depth = loop_info.get_loop_depth(curr_bb);
            let (curr_block, curr_edges) = if curr_loop_depth == group_loop_depth {
                // This block is not in a nested loop
                self.encode_block(label_prefix, curr_bb, return_block)?
            } else {
                debug_assert!(curr_loop_depth > group_loop_depth);
                let is_loop_head = loop_info.is_loop_head(curr_bb);
                if curr_loop_depth == group_loop_depth + 1 && is_loop_head {
                    // Encode a nested loop
                    self.encode_loop(label_prefix, curr_bb, return_block)?
                } else {
                    debug_assert!(curr_loop_depth > group_loop_depth + 1 || !is_loop_head);
                    // Skip the inner block of a nested loop
                    continue;
                }
            };
            bb_map.insert(curr_bb, curr_block);
            unresolved_edges.extend(curr_edges);
        }

        // Return unresolved CFG edges
        let group_head = ordered_group_blocks.get(0).map(|bb| {
            debug_assert!(
                bb_map.contains_key(bb),
                "Block {:?} (depth: {}, loop head: {}) has not been encoded \
                (group_loop_depth: {}, ordered_group_blocks: {:?})",
                bb,
                self.loop_encoder.loops().get_loop_depth(*bb),
                self.loop_encoder.loops().is_loop_head(*bb),
                group_loop_depth,
                ordered_group_blocks,
            );
            bb_map[bb]
        });
        let still_unresolved_edges =
            self.encode_unresolved_edges(unresolved_edges, |bb| bb_map.get(&bb).cloned())?;
        Ok((group_head, still_unresolved_edges))
    }

    fn encode_unresolved_edges<F: Fn(BasicBlockIndex) -> Option<CfgBlockIndex>>(
        &mut self,
        mut unresolved_edges: Vec<(CfgBlockIndex, BasicBlockIndex)>,
        resolver: F,
    ) -> SpannedEncodingResult<Vec<(CfgBlockIndex, BasicBlockIndex)>> {
        let mut still_unresolved_edges: Vec<_> = vec![];
        for (curr_block, target) in unresolved_edges.drain(..) {
            if let Some(target_block) = resolver(target) {
                self.cfg_method
                    .set_successor(curr_block, Successor::Goto(target_block));
            } else {
                still_unresolved_edges.push((curr_block, target));
            }
        }
        Ok(still_unresolved_edges)
    }

    fn stmt_preconditions(&self, stmt: &vir::Stmt) -> Vec<(Option<String>, vir::Expr)> {
        use vir::{ExprFolder, StmtWalker};
        struct FindFnApps<'a, 'b, 'c> {
            recurse: bool,
            preconds: Vec<(Option<String>, vir::Expr)>,
            encoder: &'a Encoder<'b, 'c>,
        }
        fn is_const_true(expr: &vir::Expr) -> bool {
            matches!(
                expr,
                vir::Expr::Const(vir::ConstExpr {
                    value: vir::Const::Bool(true),
                    ..
                })
            )
        }
        impl<'a, 'b, 'c> FindFnApps<'a, 'b, 'c> {
            fn push_precond(&mut self, expr: vir::Expr, fn_name: Option<String>) {
                let expr = self.fold(expr);
                if !is_const_true(&expr) {
                    self.preconds.push((fn_name, expr));
                }
            }
        }
        impl<'a, 'b, 'c> StmtWalker for FindFnApps<'a, 'b, 'c> {
            fn walk_exhale(&mut self, statement: &vir::Exhale) {
                self.push_precond(statement.expr.clone(), None);
            }
            fn walk_expr(&mut self, expr: &vir::Expr) {
                self.fold(expr.clone());
            }
        }
        impl<'a, 'b, 'c> ExprFolder for FindFnApps<'a, 'b, 'c> {
            fn fold_func_app(&mut self, expr: vir::FuncApp) -> vir::Expr {
                let vir::FuncApp {
                    function_name,
                    type_arguments,
                    arguments,
                    formal_arguments,
                    return_type,
                    ..
                } = expr;
                if self.recurse {
                    let identifier: vir::FunctionIdentifier = compute_identifier(
                        &function_name,
                        &type_arguments,
                        &formal_arguments,
                        &return_type,
                    )
                    .into();
                    let pres = self.encoder.get_function(&identifier).unwrap().pres.clone();
                    // Avoid recursively collecting preconditions: they should be self-framing anyway
                    self.recurse = false;
                    let pres: vir::Expr = pres
                        .into_iter()
                        .fold(true.into(), |acc, expr| vir_expr! { [acc] && [expr] });
                    self.push_precond(pres, Some(function_name));
                    self.recurse = true;

                    for arg in arguments {
                        self.fold(arg);
                    }
                }
                true.into()
            }
            fn fold_inhale_exhale(&mut self, expr: vir::InhaleExhale) -> vir::Expr {
                // We only care about the exhale part (e.g. for `walk_exhale`)
                self.fold(*expr.exhale_expr)
            }
            fn fold_predicate_access_predicate(
                &mut self,
                expr: vir::PredicateAccessPredicate,
            ) -> vir::Expr {
                self.fold(*expr.argument);
                true.into()
            }
            fn fold_field_access_predicate(
                &mut self,
                expr: vir::FieldAccessPredicate,
            ) -> vir::Expr {
                self.fold(*expr.base);
                true.into()
            }
            fn fold_bin_op(&mut self, expr: vir::BinOp) -> vir::Expr {
                let vir::BinOp {
                    op_kind,
                    left,
                    right,
                    position,
                } = expr;
                let left = self.fold_boxed(left);
                let right = self.fold_boxed(right);
                match op_kind {
                    vir::BinaryOpKind::And if is_const_true(&left) => *right,
                    vir::BinaryOpKind::And if is_const_true(&right) => *left,
                    vir::BinaryOpKind::Or if is_const_true(&left) => *left,
                    vir::BinaryOpKind::Or if is_const_true(&right) => *right,
                    _ => vir::Expr::BinOp(vir::BinOp {
                        op_kind,
                        left,
                        right,
                        position,
                    }),
                }
            }
        }
        let mut walker = FindFnApps {
            recurse: true,
            preconds: Vec::new(),
            encoder: self.encoder,
        };
        walker.walk(stmt);
        walker.preconds
    }
    fn block_preconditions(&self, block: &CfgBlockIndex) -> Vec<(Option<String>, vir::Expr)> {
        let bb = &self.cfg_method.basic_blocks[block.block_index];
        let mut preconds: Vec<_> = bb
            .stmts
            .iter()
            .flat_map(|stmt| self.stmt_preconditions(stmt))
            .collect();
        match &bb.successor {
            Successor::Undefined => (),
            Successor::Return => (),
            Successor::Goto(cbi) => preconds.extend(self.block_preconditions(cbi)),
            Successor::GotoSwitch(succs, def) => {
                preconds.extend(
                    succs
                        .iter()
                        .flat_map(|cond_bb| self.block_preconditions(&cond_bb.1)),
                );
                preconds.extend(self.block_preconditions(def));
            }
        }
        preconds
    }
    fn block_assert_to_assume(&mut self, block: &CfgBlockIndex) {
        let bb = &mut self.cfg_method.basic_blocks[block.block_index];
        for stmt in &mut bb.stmts {
            if let vir::Stmt::Assert(assert) = stmt {
                let expr = assert.expr.clone();
                *stmt = vir::Stmt::Inhale(vir::Inhale { expr });
            }
        }
        match bb.successor.clone() {
            Successor::Undefined => (),
            Successor::Return => (),
            Successor::Goto(cbi) => self.block_assert_to_assume(&cbi),
            Successor::GotoSwitch(succs, def) => {
                for (_, succ) in succs {
                    self.block_assert_to_assume(&succ);
                }
                self.block_assert_to_assume(&def)
            }
        }
    }

    /// Encodes a loop.
    ///
    /// Returns:
    /// * The first CFG block of the encoding
    /// * A vector of unresolved CFG edges
    ///
    /// The encoding transforms
    /// ```text
    /// while { g = G; g } { B1; invariant!(I); B2 }
    /// ```
    /// into
    /// ```text
    /// g = G
    /// if (g) {
    ///   B1
    ///   exhale I
    ///   // ... havoc local variables modified in G, B1, or B2
    ///   inhale I
    ///   B2
    ///   g = G
    ///   if (g) {
    ///     B1
    ///     exhale I
    ///     assume false
    ///   }
    /// }
    /// assume !g
    /// ```
    #[tracing::instrument(level = "debug", skip(self))]
    fn encode_loop(
        &mut self,
        label_prefix: &str,
        loop_head: BasicBlockIndex,
        return_block: CfgBlockIndex,
    ) -> SpannedEncodingResult<(CfgBlockIndex, Vec<(CfgBlockIndex, BasicBlockIndex)>)> {
        let loop_info = self.loop_encoder.loops();
        debug_assert!(loop_info.is_loop_head(loop_head));
        let loop_label_prefix = format!("{}loop{}", label_prefix, loop_head.index());
        let loop_depth = loop_info.get_loop_head_depth(loop_head);

        let loop_body: Vec<BasicBlockIndex> = loop_info
            .get_loop_body(loop_head)
            .iter()
            .copied()
            .filter(|&bb| {
                self.procedure.is_reachable_block(bb) && !self.procedure.is_spec_block(bb)
            })
            .collect();

        // Identify important blocks
        let loop_exit_blocks = loop_info.get_loop_exit_blocks(loop_head);
        let loop_exit_blocks_set: FxHashSet<_> = loop_exit_blocks.iter().cloned().collect();
        let before_invariant_block: BasicBlockIndex = self.cached_loop_invariant_block[&loop_head];
        let before_inv_block_pos = loop_body
            .iter()
            .copied()
            .position(|bb| bb == before_invariant_block)
            .unwrap();
        let after_inv_block_pos = 1 + before_inv_block_pos;
        // Find boolean switch exit blocks before the invariant
        let boolean_exit_blocks_before_inv: Vec<_> = loop_body[0..after_inv_block_pos]
            .iter()
            .copied()
            .filter(|bb| loop_exit_blocks_set.contains(bb))
            .filter(|&bb| self.procedure.successors(bb).len() == 2)
            .collect();
        // HEURISTIC: pick the last boolean exit block before the invariant.
        // An infinite loop will have no exit blocks, so we have to use an Option here
        let opt_loop_guard_switch = boolean_exit_blocks_before_inv.last().cloned();
        let after_guard_block_pos = opt_loop_guard_switch
            .and_then(|loop_guard_switch| {
                loop_body
                    .iter()
                    .position(|&bb| bb == loop_guard_switch)
                    .map(|x| x + 1)
            })
            .unwrap_or(0);
        let after_guard_block = loop_body[after_guard_block_pos];
        let after_inv_block = loop_body[after_inv_block_pos];
        let loop_head_span = self.mir_encoder.get_span_of_basic_block(loop_head);

        debug!("loop_head: {:?}", loop_head);
        debug!("loop_body: {:?}", loop_body);
        debug!("opt_loop_guard_switch: {:?}", opt_loop_guard_switch);
        debug!("before_invariant_block: {:?}", before_invariant_block);
        debug!("after_guard_block: {:?}", after_guard_block);
        debug!("after_inv_block: {:?}", after_inv_block);
        if loop_info.is_conditional_branch(loop_head, before_invariant_block) {
            debug!(
                "{:?} is conditional branch in loop {:?}",
                before_invariant_block, loop_head
            );
            let loop_head_span = self.mir_encoder.get_span_of_basic_block(loop_head);
            return Err(SpannedEncodingError::incorrect(
                "the loop invariant cannot be in a conditional branch of the loop",
                loop_body
                    .iter()
                    .map(|&bb| self.mir_encoder.get_span_of_basic_block(bb))
                    .filter(|&span| span.contains(loop_head_span))
                    .min()
                    .unwrap(),
            ));
        }

        // Split the blocks such that:
        // * G is loop_guard_evaluation, starting (if nonempty) with loop_head
        // * B1 is loop_body_before_inv, starting with after_guard_block (which could be loop_head)
        // * B2 is loop_body_after_inv, starting with after_inv_block
        let loop_guard_evaluation = &loop_body[0..after_guard_block_pos];
        let loop_body_before_inv = &loop_body[after_guard_block_pos..after_inv_block_pos];
        let loop_body_after_inv = &loop_body[after_inv_block_pos..];

        // The main path in the encoding is: start -> G -> B1 -> invariant -> B2 -> G -> B1 -> end
        // We are going to build the encoding left to right.
        let mut heads = vec![];

        // Build the "start" CFG block (*start* - G - B1 - invariant - B2 - G - B1 - end)
        let start_block = self.cfg_method.add_block(
            &format!("{loop_label_prefix}_start"),
            vec![vir::Stmt::comment(format!(
                "========== {loop_label_prefix}_start =========="
            ))],
        );
        heads.push(Some(start_block));

        // Encode the first G group (start - *G* - B1 - invariant - B2 - G - B1 - end)
        let (first_g_head, first_g_edges) = self.encode_blocks_group(
            &format!("{loop_label_prefix}_group1_"),
            loop_guard_evaluation,
            loop_depth,
            return_block,
        )?;
        heads.push(first_g_head);

        // Encode the first B1 group (start - G - *B1* - invariant - B2 - G - B1 - end)
        let (first_b1_head, first_b1_edges) = self.encode_blocks_group(
            &format!("{loop_label_prefix}_group2_"),
            loop_body_before_inv,
            loop_depth,
            return_block,
        )?;
        heads.push(first_b1_head);

        // Calculate if `G` and `B1` are safe to include as the first `body_invariant!(...)`
        let mut preconds = first_g_head
            .map(|cbi| self.block_preconditions(&cbi))
            .unwrap_or_default();
        preconds.extend(
            first_b1_head
                .map(|cbi| self.block_preconditions(&cbi))
                .unwrap_or_default(),
        );

        // Build the "invariant" CFG block (start - G - B1 - *invariant* - B2 - G - B1 - end)
        // (1) checks the loop invariant on entry
        // (2) havocs the invariant and the local variables.
        let inv_pre_block = self.cfg_method.add_block(
            &format!("{loop_label_prefix}_inv_pre"),
            vec![vir::Stmt::comment(format!(
                "========== {loop_label_prefix}_inv_pre =========="
            ))],
        );
        let inv_post_block_perms = self.cfg_method.add_block(
            &format!("{loop_label_prefix}_inv_post_perm"),
            vec![vir::Stmt::comment(format!(
                "========== {loop_label_prefix}_inv_post_perm =========="
            ))],
        );
        let inv_post_block_fnspc = self.cfg_method.add_block(
            &format!("{loop_label_prefix}_inv_post_fnspc"),
            vec![vir::Stmt::comment(format!(
                "========== {loop_label_prefix}_inv_post_fnspc =========="
            ))],
        );
        heads.push(Some(inv_pre_block));
        self.cfg_method
            .set_successor(inv_pre_block, vir::Successor::Goto(inv_post_block_perms));
        {
            let stmts =
                self.encode_loop_invariant_exhale_stmts(loop_head, before_invariant_block, false)?;
            self.cfg_method.add_stmts(inv_pre_block, stmts);
        }
        // We'll add later more statements at the end of inv_pre_block, to havoc local variables
        let fnspec_span = {
            let (stmts, fnspec_span) = self.encode_loop_invariant_inhale_fnspec_stmts(
                loop_head,
                before_invariant_block,
                false,
            )?;
            self.cfg_method.add_stmts(inv_post_block_fnspc, stmts);
            fnspec_span
        };
        {
            let stmts = self
                .encode_loop_invariant_inhale_perm_stmts(loop_head, before_invariant_block, false)
                .with_span(fnspec_span)?;
            self.cfg_method.add_stmts(inv_post_block_perms, stmts);
        }

        let mid_groups = if preconds.is_empty() {
            // Encode the mid G group (start - G - B1 - invariant_perm - *G* - B1 - invariant_fnspec - B2 - G - B1 - end)
            let mid_g = self.encode_blocks_group(
                &format!("{loop_label_prefix}_group2a_"),
                loop_guard_evaluation,
                loop_depth,
                return_block,
            )?;
            if let Some(mid_g_head) = &mid_g.0 {
                self.block_assert_to_assume(mid_g_head);
            }

            // Encode the mid B1 group (start - G - B1 - invariant_perm - G - *B1* - invariant_fnspec - B2 - G - B1 - end)
            let mid_b1 = self.encode_blocks_group(
                &format!("{loop_label_prefix}_group2b_"),
                loop_body_before_inv,
                loop_depth,
                return_block,
            )?;
            if let Some(mid_b1_head) = &mid_b1.0 {
                self.block_assert_to_assume(mid_b1_head);
            }
            // Save for later linking up
            Some((mid_g, mid_b1))
        } else {
            // Cannot add loop guard to loop invariant
            let fn_names: Vec<_> = preconds
                .iter()
                .filter_map(|(name, _)| name.as_ref())
                .map(|name| {
                    if let Some(rust_name) = name.strip_prefix("f_") {
                        return rust_name;
                    };
                    name.strip_prefix("m_").unwrap_or(name)
                })
                .collect();
            let warning_msg = if fn_names.is_empty() {
                "the loop guard was not automatically added as a `body_invariant!(...)`, consider doing this manually".to_string()
            } else {
                "the loop guard was not automatically added as a `body_invariant!(...)`, \
                due to the following pure functions with preconditions: ["
                    .to_string()
                    + &fn_names.join(", ")
                    + "]"
            };
            // Span of loop guard
            let span_lg = loop_guard_evaluation
                .last()
                .map(|bb| self.mir_encoder.get_span_of_basic_block(*bb));
            // Span of entire loop body before inv; the last elem (if any) will be the `body_invariant!(...)` bb
            let span_lb = loop_body_before_inv
                .iter()
                .rev()
                .skip(1)
                .map(|bb| self.mir_encoder.get_span_of_basic_block(*bb))
                .fold(None, |acc: Option<Span>, span| {
                    Some(
                        acc.map(|other| {
                            if span.ctxt() == other.ctxt() {
                                span.to(other)
                            } else {
                                other
                            }
                        })
                        .unwrap_or(span),
                    )
                });
            // Multispan to highlight both
            let span =
                MultiSpan::from_spans(vec![span_lg, span_lb].into_iter().flatten().collect());
            // It's only a warning so we might as well emit it straight away
            PrustiError::warning(warning_msg, span).emit(&self.encoder.env().diagnostic);
            None
        };

        // Encode the last B2 group (start - G - B1 - invariant - *B2* - G - B1 - end)
        let (last_b2_head, last_b2_edges) = self.encode_blocks_group(
            &format!("{loop_label_prefix}_group3_"),
            loop_body_after_inv,
            loop_depth,
            return_block,
        )?;
        heads.push(last_b2_head);

        // Encode the last G group (start - G - B1 - invariant - B2 - *G* - B1 - end)
        let (last_g_head, last_g_edges) = self.encode_blocks_group(
            &format!("{loop_label_prefix}_group4_"),
            loop_guard_evaluation,
            loop_depth,
            return_block,
        )?;
        heads.push(last_g_head);

        // Encode the last B1 group (start - G - B1 - invariant - B2 - G - *B1* - end)
        let (last_b1_head, last_b1_edges) = self.encode_blocks_group(
            &format!("{loop_label_prefix}_group5_"),
            loop_body_before_inv,
            loop_depth,
            return_block,
        )?;
        heads.push(last_b1_head);

        // Build the "end" CFG block (start - G - B1 - invariant - B2 - G - B1 - *end*)
        // (1) checks the invariant after one loop iteration
        // (2) kills the program path with an `assume false`
        let end_body_block = self.cfg_method.add_block(
            &format!("{loop_label_prefix}_end_body"),
            vec![vir::Stmt::comment(format!(
                "========== {loop_label_prefix}_end_body =========="
            ))],
        );
        {
            let stmts =
                self.encode_loop_invariant_exhale_stmts(loop_head, before_invariant_block, true)?;
            self.cfg_method.add_stmts(end_body_block, stmts);
        }
        self.cfg_method.add_stmt(
            end_body_block,
            vir::Stmt::Inhale(vir::Inhale { expr: false.into() }),
        );
        heads.push(Some(end_body_block));

        // We are going to link the unresolved edges.
        let mut still_unresolved_edges = vec![];

        // Link edges of "start" (*start* - G - B1 - invariant - B2 - G - B1 - end)
        let following_block = heads[1..].iter().find(|x| x.is_some()).unwrap().unwrap();
        self.cfg_method
            .set_successor(start_block, vir::Successor::Goto(following_block));

        // Link edges from the first G group (start - *G* - B1 - invariant - B2 - G - B1 - end)
        let following_block = heads[2..].iter().find(|x| x.is_some()).unwrap().unwrap();
        still_unresolved_edges.extend(self.encode_unresolved_edges(first_g_edges, |bb| {
            if bb == after_guard_block {
                Some(following_block)
            } else {
                None
            }
        })?);

        // Link edges from the first B1 group (start - G - *B1* - invariant - B2 - G - B1 - end)
        let following_block = heads[3..].iter().find(|x| x.is_some()).unwrap().unwrap();
        still_unresolved_edges.extend(self.encode_unresolved_edges(first_b1_edges, |bb| {
            if bb == after_inv_block {
                Some(following_block)
            } else {
                None
            }
        })?);

        if let Some(((mid_g_head, mid_g_edges), (mid_b1_head, mid_b1_edges))) = mid_groups {
            let mid_b1_block = mid_b1_head.unwrap_or(inv_post_block_fnspc);
            // Link edges of "invariant_perm" (start - G - B1 - *invariant_perm* - G - B1 - invariant_fnspec - B2 - G - B1 - end)
            self.cfg_method.set_successor(
                inv_post_block_perms,
                vir::Successor::Goto(mid_g_head.unwrap_or(mid_b1_block)),
            );

            // We know that there is at least one loop iteration of B2, thus it is safe to assume
            // that anything beforehand couldn't have exited the loop. Here we use
            // `self.cfg_method.set_successor(..., Successor::Return)` as the same as `assume false`
            for (curr_block, target) in &mid_g_edges {
                if self.loop_encoder.get_loop_depth(*target) < loop_depth {
                    self.cfg_method
                        .set_successor(*curr_block, Successor::Return);
                }
            }
            let mid_g_edges = mid_g_edges
                .into_iter()
                .filter(|(_, target)| self.loop_encoder.get_loop_depth(*target) >= loop_depth)
                .collect::<Vec<_>>();
            // Link edges from the mid G group (start - G - B1 - invariant_perm - *G* - B1 - invariant_fnspec - B2 - G - B1 - end)
            still_unresolved_edges.extend(self.encode_unresolved_edges(mid_g_edges, |bb| {
                if bb == after_guard_block {
                    Some(mid_b1_block)
                } else {
                    None
                }
            })?);

            // We know that there is at least one loop iteration of B2, thus it is safe to assume
            // that anything beforehand couldn't have exited the loop.
            for (curr_block, target) in &mid_b1_edges {
                if self.loop_encoder.get_loop_depth(*target) < loop_depth {
                    self.cfg_method
                        .set_successor(*curr_block, Successor::Return);
                }
            }
            let mid_b1_edges = mid_b1_edges
                .into_iter()
                .filter(|(_, target)| self.loop_encoder.get_loop_depth(*target) >= loop_depth)
                .collect::<Vec<_>>();
            // Link edges from the mid B1 group (start - G - B1 - invariant_perm - G - *B1* - invariant_fnspec - B2 - G - B1 - end)
            still_unresolved_edges.extend(self.encode_unresolved_edges(mid_b1_edges, |bb| {
                if bb == after_inv_block {
                    Some(inv_post_block_fnspc)
                } else {
                    None
                }
            })?);
        } else {
            // Link edges of "invariant_perm" (start - G - B1 - *invariant_perm* - invariant_fnspec - B2 - G - B1 - end)
            self.cfg_method.set_successor(
                inv_post_block_perms,
                vir::Successor::Goto(inv_post_block_fnspc),
            );
        }

        // Link edges of "invariant" (start - G - B1 - *invariant* - B2 - G - B1 - end)
        let following_block = heads[4..].iter().find(|x| x.is_some()).unwrap().unwrap();
        self.cfg_method
            .set_successor(inv_post_block_fnspc, vir::Successor::Goto(following_block));

        // Link edges from the last B2 group (start - G - B1 - invariant - *B2* - G - B1 - end)
        let following_block = heads[5..].iter().find(|x| x.is_some()).unwrap().unwrap();
        still_unresolved_edges.extend(self.encode_unresolved_edges(last_b2_edges, |bb| {
            if bb == loop_head {
                Some(following_block)
            } else {
                None
            }
        })?);

        // Link edges from the last G group (start - G - B1 - invariant - B2 - *G* - B1 - end)
        let following_block = heads[6..].iter().find(|x| x.is_some()).unwrap().unwrap();
        still_unresolved_edges.extend(self.encode_unresolved_edges(last_g_edges, |bb| {
            if bb == after_guard_block {
                Some(following_block)
            } else {
                None
            }
        })?);

        // Link edges from the last B1 group (start - G - B1 - invariant - B2 - G - *B1* - end)
        let following_block = heads[7..].iter().find(|x| x.is_some()).unwrap().unwrap();
        still_unresolved_edges.extend(self.encode_unresolved_edges(last_b1_edges, |bb| {
            if bb == after_inv_block {
                Some(following_block)
            } else {
                None
            }
        })?);

        // Link edges of "end" (start - G - B1 - invariant - B2 - G - B1 - *end*)
        self.cfg_method
            .set_successor(end_body_block, vir::Successor::Return);

        // Final step: havoc Viper local variables assigned in the encoding of the loop body
        let vars = collect_assigned_vars(&self.cfg_method, end_body_block, inv_pre_block);
        for var in vars {
            let builtin_method = match var.typ {
                vir::Type::Int => BuiltinMethodKind::HavocInt,
                vir::Type::Bool => BuiltinMethodKind::HavocBool,
                vir::Type::Float(vir::Float::F32) => BuiltinMethodKind::HavocF32,
                vir::Type::Float(vir::Float::F64) => BuiltinMethodKind::HavocF64,
                vir::Type::BitVector(value) => BuiltinMethodKind::HavocBV(value),
                vir::Type::TypedRef(_) => BuiltinMethodKind::HavocRef,
                vir::Type::TypeVar(_) => BuiltinMethodKind::HavocRef,
                vir::Type::Domain(_) => BuiltinMethodKind::HavocRef,
                vir::Type::Snapshot(_) => BuiltinMethodKind::HavocRef,
                vir::Type::Seq(_) => BuiltinMethodKind::HavocRef,
                vir::Type::Map(_) => BuiltinMethodKind::HavocRef,
                vir::Type::Ref => {
                    return Err(SpannedEncodingError::internal(
                        format!("unexpected type of local variable {var:?}"),
                        self.mir.span,
                    ))
                }
            };
            let stmt = vir::Stmt::MethodCall(vir::MethodCall {
                method_name: self
                    .encoder
                    .encode_builtin_method_use(builtin_method)
                    .with_span(loop_head_span)?,
                arguments: vec![],
                targets: vec![var],
            });
            self.cfg_method.add_stmt(inv_pre_block, stmt);
        }

        // Done. Phew!
        Ok((start_block, still_unresolved_edges))
    }

    /// Encode a block.
    ///
    /// Returns:
    /// * The head of the encoded block
    /// * A vector unresolved edges
    #[tracing::instrument(level = "debug", skip(self))]
    fn encode_block(
        &mut self,
        label_prefix: &str,
        bbi: BasicBlockIndex,
        return_block: CfgBlockIndex,
    ) -> SpannedEncodingResult<(CfgBlockIndex, Vec<(CfgBlockIndex, BasicBlockIndex)>)> {
        debug_assert!(!self.procedure.is_spec_block(bbi));

        let curr_block = self.cfg_method.add_block(
            &format!("{label_prefix}{bbi:?}"),
            vec![vir::Stmt::comment(format!(
                "========== {label_prefix}{bbi:?} =========="
            ))],
        );
        self.cfg_blocks_map
            .entry(bbi)
            .or_default()
            .insert(curr_block);

        if self.loop_encoder.is_loop_head(bbi) {
            self.cfg_method
                .add_stmt(curr_block, vir::Stmt::comment("This is a loop head"));
        }

        self.encode_execution_flag(bbi, curr_block)?;
        let opt_successor = self.encode_block_statements(bbi, curr_block)?;
        let mir_successor: MirSuccessor = if let Some(successor) = opt_successor {
            // In case of unsupported statements, we do not encode the terminator
            successor
        } else {
            self.encode_block_terminator(bbi, curr_block)?
        };

        // Make sure that the
        let mir_targets = mir_successor.targets();
        // Force the encoding of a block if there is more than one successor, to leave
        // space for the fold-unfold algorithm.
        let force_block_on_edge = mir_targets.len() > 1;
        let mut targets_map = FxHashMap::default();
        let mut complete_resolution = true;
        for &target in &mir_targets {
            let opt_edge_block = self.encode_edge_block(bbi, target, force_block_on_edge)?;
            if let Some(edge_block) = opt_edge_block {
                targets_map.insert(target, edge_block);
            } else {
                complete_resolution = false;
            }
        }
        let unresolved_edges = if complete_resolution {
            // Resolve successor and return the edge blocks
            let curr_successor =
                mir_successor.encode(return_block, |target_bb| targets_map[&target_bb]);
            self.cfg_method.set_successor(curr_block, curr_successor);
            // This can be empty, if there are no unresolved edges left
            targets_map
                .iter()
                .map(|(&target, &edge_block)| (edge_block, target))
                .collect()
        } else {
            match mir_successor {
                MirSuccessor::Goto(target) => vec![(curr_block, target)],
                MirSuccessor::GotoSwitch(guarded_targets, default_target) => {
                    debug_assert!(guarded_targets.is_empty());
                    vec![(curr_block, default_target)]
                }
                x => unreachable!("{:?}", x),
            }
        };

        Ok((curr_block, unresolved_edges))
    }

    /// Store a flag that becomes true the first time the block is executed
    fn encode_execution_flag(
        &mut self,
        bbi: BasicBlockIndex,
        cfg_block: CfgBlockIndex,
    ) -> SpannedEncodingResult<()> {
        let pos = self
            .mir_encoder
            .register_span(self.mir_encoder.get_span_of_basic_block(bbi));
        let executed_flag_var = self.cfg_block_has_been_executed[&bbi].clone();
        self.cfg_method.add_stmt(
            cfg_block,
            vir::Stmt::Assign(vir::Assign {
                target: vir::Expr::local(executed_flag_var).set_pos(pos),
                source: true.into(),
                kind: vir::AssignKind::Copy,
            }),
        );
        Ok(())
    }

    /// Encode the statements of the block.
    /// In case of unsupported statements, this function will return `MirSuccessor::Kill`.
    #[tracing::instrument(level = "debug", skip(self))]
    fn encode_block_statements(
        &mut self,
        bbi: BasicBlockIndex,
        cfg_block: CfgBlockIndex,
    ) -> SpannedEncodingResult<Option<MirSuccessor>> {
        debug_assert!(!self.procedure.is_spec_block(bbi));
        let bb_data = &self.mir.basic_blocks[bbi];
        let statements: &Vec<mir::Statement<'tcx>> = &bb_data.statements;
        for stmt_index in 0..statements.len() {
            trace!("Encode statement {:?}:{}", bbi, stmt_index);
            let location = mir::Location {
                block: bbi,
                statement_index: stmt_index,
            };
            {
                let (stmts, opt_succ) = self.encode_statement_at(location)?;
                debug_assert!(matches!(opt_succ, None | Some(MirSuccessor::Kill)));
                self.cfg_method.add_stmts(cfg_block, stmts);
                if opt_succ.is_some() {
                    // If the statement is unsupported, we stop encoding the block.
                    // The fold-unfold would probably fail on the code after the unsupported
                    // statement.
                    return Ok(opt_succ);
                }
            }
            {
                let stmts = self.encode_expiring_borrows_at(location)?;
                self.cfg_method.add_stmts(cfg_block, stmts);
            }
        }
        Ok(None)
    }

    /// Encode the terminator of the block
    #[tracing::instrument(level = "debug", skip(self))]
    fn encode_block_terminator(
        &mut self,
        bbi: BasicBlockIndex,
        curr_block: CfgBlockIndex,
    ) -> SpannedEncodingResult<MirSuccessor> {
        let bb_data = &self.mir.basic_blocks[bbi];
        let location = mir::Location {
            block: bbi,
            statement_index: bb_data.statements.len(),
        };
        let (stmts, opt_mir_successor) = self.encode_statement_at(location)?;
        self.cfg_method.add_stmts(curr_block, stmts);
        Ok(opt_mir_successor.unwrap())
    }

    /// Encode a MIR statement or terminator, encoding an `assert false` in case
    /// of usage of unsupported features.
    #[tracing::instrument(level = "debug", skip(self))]
    fn encode_statement_at(
        &mut self,
        location: mir::Location,
    ) -> SpannedEncodingResult<(Vec<vir::Stmt>, Option<MirSuccessor>)> {
        let span = self.mir_encoder.get_span_of_location(location);
        let bb_data = &self.mir[location.block];
        let index = location.statement_index;
        let stmts_succ_res = if index < bb_data.statements.len() {
            let mir_stmt = &bb_data.statements[index];
            self.encode_statement(mir_stmt, location)
                .map(|stmts| (stmts, None))
        } else {
            let mir_term = bb_data.terminator();
            self.encode_terminator(mir_term, location)
                .map(|(stmts, succ)| (stmts, Some(succ)))
        };

        // Intercept encoding error caused by an unsupported feature
        let (stmts, successor) = match stmts_succ_res {
            Ok(stmts_succ) => stmts_succ,
            Err(err) => {
                let unsupported_msg = match err.kind() {
                    EncodingErrorKind::Unsupported(msg)
                        if config::allow_unreachable_unsupported_code() =>
                    {
                        msg.to_string()
                    }
                    _ => {
                        // Propagate the error
                        return Err(err);
                    }
                };
                // TODO: How to combine this with the span of the encoding error?
                let err_ctxt = ErrorCtxt::Unsupported(unsupported_msg.clone());
                let pos = self.register_error(span, err_ctxt);
                let head_stmt = if index < bb_data.statements.len() {
                    format!("[mir] {:?}", &bb_data.statements[index])
                } else {
                    format!("[mir] {:?}", bb_data.terminator())
                };
                let stmts = vec![
                    vir::Stmt::comment(head_stmt),
                    vir::Stmt::comment(format!("Unsupported feature: {unsupported_msg}")),
                    vir::Stmt::Assert(vir::Assert {
                        expr: false.into(),
                        position: pos,
                    }),
                ];
                (stmts, Some(MirSuccessor::Kill))
            }
        };
        Ok((self.set_stmts_default_pos(stmts, span), successor))
    }

    /// Note: it's better to call `encode_statement_at` instead of this method.
    #[tracing::instrument(level = "debug", skip(self), fields(statement = ?stmt.kind, span = ?stmt.source_info.span))]
    fn encode_statement(
        &mut self,
        stmt: &mir::Statement<'tcx>,
        location: mir::Location,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        let mut stmts = vec![vir::Stmt::comment(format!("[mir] {stmt:?}"))];
        let span = self.mir_encoder.get_span_of_location(location);

        let encoding_stmts = match stmt.kind {
            mir::StatementKind::StorageLive(..)
            | mir::StatementKind::StorageDead(..)
            | mir::StatementKind::FakeRead(..)
            | mir::StatementKind::AscribeUserType(..)
            | mir::StatementKind::Coverage(..)
            | mir::StatementKind::PlaceMention(..)
            | mir::StatementKind::Nop => vec![],

            mir::StatementKind::Assign(box (lhs, ref rhs)) => {
                // Array access on the LHS should always be mutable (idx is always calculated
                // before, and just a separate local variable here)
                let (lhs_place_encoding, ty, _) =
                    self.mir_encoder.encode_place(lhs).with_span(span)?;
                match lhs_place_encoding {
                    PlaceEncoding::SliceAccess {
                        box base,
                        index,
                        rust_slice_ty: rust_ty,
                        ..
                    }
                    | PlaceEncoding::ArrayAccess {
                        box base,
                        index,
                        rust_array_ty: rust_ty,
                        ..
                    } => {
                        // Current stmt is of the form `arr[idx] = val`. This does not have an expiring
                        // temporary variable, so we encode it differently from indexing into an array.
                        self.encode_array_direct_assign(base, index, rust_ty, rhs, location)?
                    }
                    _ => {
                        let (encoded_lhs, pre_stmts) = self
                            .postprocess_place_encoding(
                                lhs_place_encoding,
                                ArrayAccessKind::Mutable(None, location),
                            )
                            .with_span(span)?;
                        stmts.extend(pre_stmts);
                        self.encode_assign(encoded_lhs, rhs, ty, location)?
                    }
                }
            }
            ref x => {
                return Err(SpannedEncodingError::unsupported(
                    format!("unsupported statement kind: {x:?}"),
                    span,
                ))
            }
        };
        stmts.extend(encoding_stmts);
        Ok(self.set_stmts_default_pos(stmts, stmt.source_info.span))
    }

    fn set_stmts_default_pos(&self, stmts: Vec<vir::Stmt>, default_span: Span) -> Vec<vir::Stmt> {
        let pos = self
            .encoder
            .error_manager()
            .register_span(self.proc_def_id, default_span);
        stmts.into_iter().map(|s| s.set_default_pos(pos)).collect()
    }

    /// Encode assignment of RHS to LHS, depending on what kind of thing the RHS is
    fn encode_assign(
        &mut self,
        encoded_lhs: vir::Expr,
        rhs: &mir::Rvalue<'tcx>,
        ty: ty::Ty<'tcx>,
        location: mir::Location,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        let span = self.mir_encoder.get_span_of_location(location);

        Ok(match *rhs {
            mir::Rvalue::Use(ref operand) => {
                self.encode_assign_operand(&encoded_lhs, operand, location)?
            }
            mir::Rvalue::Aggregate(ref aggregate, ref operands) => self.encode_assign_aggregate(
                &encoded_lhs,
                ty,
                aggregate,
                operands.as_slice(),
                location,
            )?,
            mir::Rvalue::BinaryOp(op, box (ref left, ref right)) => {
                self.encode_assign_binary_op(op, left, right, encoded_lhs, ty, location)?
            }
            mir::Rvalue::CheckedBinaryOp(op, box (ref left, ref right)) => {
                self.encode_assign_checked_binary_op(op, left, right, encoded_lhs, ty, location)?
            }
            mir::Rvalue::UnaryOp(op, ref operand) => {
                self.encode_assign_unary_op(op, operand, encoded_lhs, ty, location)?
            }
            mir::Rvalue::NullaryOp(ref op, op_ty) => {
                self.encode_assign_nullary_op(op, op_ty, encoded_lhs, ty, location)?
            }
            mir::Rvalue::Discriminant(src) => {
                self.encode_assign_discriminant(src, location, encoded_lhs, ty)?
            }
            mir::Rvalue::Ref(_region, mir_borrow_kind, place) => {
                self.encode_assign_ref(mir_borrow_kind, place, location, encoded_lhs, ty)?
            }
            mir::Rvalue::Cast(mir::CastKind::PointerExposeAddress, ref operand, dst_ty)
            | mir::Rvalue::Cast(mir::CastKind::PointerFromExposedAddress, ref operand, dst_ty)
            | mir::Rvalue::Cast(mir::CastKind::IntToInt, ref operand, dst_ty) => {
                self.encode_cast(operand, dst_ty, encoded_lhs, ty, location)?
            }
            mir::Rvalue::Len(place) => {
                self.encode_assign_sequence_len(encoded_lhs, place, ty, location)?
            }
            mir::Rvalue::Repeat(ref operand, times) => self
                .encode_assign_array_repeat_initializer(
                    encoded_lhs,
                    operand,
                    times,
                    ty,
                    location,
                )?,
            mir::Rvalue::Cast(
                mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize),
                ref operand,
                cast_ty,
            ) => {
                let rhs_ty = self.mir_encoder.get_operand_ty(operand);
                if rhs_ty.is_array_ref() && cast_ty.is_slice_ref() {
                    trace!("slice: operand={:?}, ty={:?}", operand, cast_ty);
                    self.encode_assign_slice(encoded_lhs, operand, cast_ty, location)?
                } else {
                    return Err(SpannedEncodingError::unsupported(
                        format!("unsizing a {rhs_ty} into a {cast_ty} is not supported"),
                        span,
                    ));
                }
            }
            mir::Rvalue::Cast(mir::CastKind::PointerCoercion(_), _, _)
            | mir::Rvalue::Cast(mir::CastKind::DynStar, _, _) => {
                return Err(SpannedEncodingError::unsupported(
                    "raw pointers are not supported",
                    span,
                ));
            }
            mir::Rvalue::Cast(cast_kind, _, _) => {
                return Err(SpannedEncodingError::unsupported(
                    format!("casts {cast_kind:?} are not supported"),
                    span,
                ));
            }
            mir::Rvalue::AddressOf(_, _) => {
                return Err(SpannedEncodingError::unsupported(
                    "raw addresses of expressions and casts from references to raw pointers are not supported", span
                ));
            }
            mir::Rvalue::ThreadLocalRef(_) => {
                return Err(SpannedEncodingError::unsupported(
                    "references to thread-local storage are not supported",
                    span,
                ));
            }
            mir::Rvalue::ShallowInitBox(_, op_ty) => {
                self.encode_assign_box(op_ty, encoded_lhs, ty, location)?
            }
            mir::Rvalue::CopyForDeref(ref place) => {
                self.encode_assign_operand(&encoded_lhs, &mir::Operand::Copy(*place), location)?
            }
        })
    }

    /// Generate an unsupported encoding error for unhandled borrow kinds.
    fn unsupported_borrow_kind(kind: mir::BorrowKind) -> EncodingError {
        match kind {
            mir::BorrowKind::Shallow => {
                EncodingError::unsupported(
                    "unsupported creation of shallow borrows (implicitly created when lowering matches)",
                )
            }
            _ => unreachable!(),
        }
    }

    /// Encode the lhs and the rhs of the assignment that create the loan
    #[tracing::instrument(level = "debug", skip(self))]
    fn encode_loan_places(
        &mut self,
        loan_places: &LoanPlaces<'tcx>,
    ) -> SpannedEncodingResult<(vir::Expr, Option<vir::Expr>, bool, Vec<vir::Stmt>)> {
        let location = loan_places.location;
        let span = self.mir_encoder.get_span_of_location(location);

        let (expiring_base, mut stmts, expiring_ty, _) = self.encode_place(
            loan_places.dest,
            ArrayAccessKind::Mutable(None, location),
            location,
        )?;
        trace!(
            "expiring_base: {:?}",
            (&expiring_base, &stmts, &expiring_ty)
        );

        // the original encoding of arrays is with a sort-of magic temporary variable, so
        // `postprocess_place_encoding` will return `i32` here instead of Array$3$i32. so here
        // we call the mir_encoder one that returns a `PlaceEncoding`, and do the
        // postprocessing if necessary ourselves.
        if let mir::Rvalue::Ref(_, mir::BorrowKind::Mut { .. }, rhs_place) = loan_places.source {
            let (rhs_place_encoding, ..) = self.mir_encoder.encode_place(rhs_place).unwrap();
            if let PlaceEncoding::ArrayAccess { .. } = rhs_place_encoding {
                // encode expiry of the array borrow
                let (expired_expr, regained_array, wand_rhs) =
                    self.array_magic_wand_at[&location].clone();

                // expiring base is something like ref$i32, so we need .val_ref.val_int
                let deref = self
                    .encoder
                    .encode_value_expr(expiring_base.clone(), expiring_ty)
                    .with_span(span)?;
                let target_ty = expiring_ty.peel_refs();
                let expiring_base_value = self
                    .encoder
                    .encode_value_expr(deref, target_ty)
                    .with_span(span)?;

                // the original magic wand refered to the temporary variable that we created for array
                // encoding. the expiry here refers to the non-temporary rust variable, so we need
                // to replace that in the wand RHS
                let wand_rhs = wand_rhs.replace_place(&expired_expr, &expiring_base_value);

                // we can't refer to the somewhat magic "lhs" label here, because there is no wand,
                // so there's no LHS. instead, we add a label just before the inhale, and refer to
                // that
                let new_lhs_label = self.cfg_method.get_fresh_label_name();
                stmts.push(vir::Stmt::label(new_lhs_label.clone()));

                let wand_rhs_patched_lhs = wand_rhs.map_old_expr_label(|label| {
                    if label == "lhs" {
                        trace!("{} -> {}", label, new_lhs_label);
                        new_lhs_label.clone()
                    } else {
                        label
                    }
                });

                let expiring_base_pred = self
                    .mir_encoder
                    .encode_place_predicate_permission(
                        expiring_base.clone(),
                        vir::PermAmount::Write,
                    )
                    .unwrap();
                stmts.push(vir_stmt! { exhale [expiring_base_pred] });

                let arr_pred =
                    vir::Expr::pred_permission(regained_array.clone(), vir::PermAmount::Write)
                        .unwrap();
                stmts.push(vir_stmt! { inhale [arr_pred] });
                stmts.push(vir_stmt! { inhale [wand_rhs_patched_lhs] });

                // NOTE: the third tuple elem is called is_mut in
                // `construct_vir_reborrowing_node_for_assignment`, and is currently only used to
                // determine whether to call `encode_transfer_permissions`. while this is a mutable
                // array access, we don't want that call, as we transfer the permissions ourselves
                // here already (because we need them for the wand RHS), so transfering them again
                // would fail.
                return Ok((expiring_base, Some(regained_array), false, stmts));
            }
        }

        let mut encode = |rhs_place,
                          stmts: &mut Vec<vir::Stmt>,
                          array_encode_kind|
         -> SpannedEncodingResult<_> {
            let (restored, pre_stmts, _, _) =
                self.encode_place(rhs_place, array_encode_kind, location)?;
            stmts.extend(pre_stmts);
            let ref_field = self
                .encoder
                .encode_value_field(expiring_ty)
                .with_span(span)?;
            let expiring = expiring_base.clone().field(ref_field.clone());
            Ok((expiring, restored, ref_field))
        };
        Ok(match loan_places.source {
            mir::Rvalue::Ref(_, mir_borrow_kind, rhs_place) => {
                let is_mut = match mir_borrow_kind {
                    mir::BorrowKind::Shared => false,
                    mir::BorrowKind::Mut { .. } => true,
                    _ => return Err(Self::unsupported_borrow_kind(mir_borrow_kind).with_span(span)),
                };
                let array_encode_kind = if is_mut {
                    ArrayAccessKind::Mutable(None, location)
                } else {
                    ArrayAccessKind::Shared
                };
                let (expiring, restored, _) = encode(rhs_place, &mut stmts, array_encode_kind)?;
                assert_eq!(expiring.get_type(), restored.get_type());
                (expiring, Some(restored), is_mut, stmts)
            }
            mir::Rvalue::Use(mir::Operand::Move(rhs_place)) => {
                let (expiring, restored_base, ref_field) =
                    encode(rhs_place, &mut stmts, ArrayAccessKind::Shared)?;
                let restored = restored_base.field(ref_field);
                assert_eq!(expiring.get_type(), restored.get_type());
                (expiring, Some(restored), true, stmts)
            }
            mir::Rvalue::Use(mir::Operand::Copy(rhs_place)) => {
                let (expiring, restored_base, ref_field) =
                    encode(rhs_place, &mut stmts, ArrayAccessKind::Shared)?;
                let restored = restored_base.field(ref_field);
                assert_eq!(expiring.get_type(), restored.get_type());
                (expiring, Some(restored), false, stmts)
            }

            mir::Rvalue::Cast(
                mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize),
                ref operand,
                ty,
            ) => {
                trace!("cast: operand={:?}, ty={:?}", operand, ty);
                let place = match *operand {
                    mir::Operand::Move(place) => place,
                    mir::Operand::Copy(place) => place,
                    _ => unreachable!("operand: {:?}", operand),
                };
                let (restored, r_stmts, ..) =
                    self.encode_place(place, ArrayAccessKind::Shared, location)?;
                stmts.extend(r_stmts);

                (expiring_base, Some(restored), false, stmts)
            }

            mir::Rvalue::Use(mir::Operand::Constant(ref expr)) => {
                // TODO: Encoding of string literals is not yet supported, so
                // do not return an expression in restored here.
                let restored: Option<vir::Expr> = if is_str(expr.ty()) {
                    None
                } else {
                    Some(
                        self.encoder
                            .encode_const_expr(expr.ty(), expr.literal)
                            .with_span(span)?,
                    )
                };

                (expiring_base, restored, false, stmts)
            }

            ref x => unreachable!("Borrow restores value {:?}", x),
        })
    }

    fn encode_transfer_permissions(
        &mut self,
        lhs: vir::Expr,
        rhs: vir::Expr,
        location: mir::Location,
        is_in_package_stmt: bool,
    ) -> Vec<vir::Stmt> {
        let mut stmts = if let Some(var) = self.old_to_ghost_var.get(&rhs) {
            vec![vir::Stmt::Assign(vir::Assign {
                target: var.clone(),
                source: lhs.clone(),
                kind: vir::AssignKind::Move,
            })]
        } else {
            vec![vir::Stmt::TransferPerm(vir::TransferPerm {
                left: lhs.clone(),
                right: rhs.clone(),
                unchecked: false,
            })]
        };

        if self.check_foldunfold_state && !is_in_package_stmt {
            let pos =
                self.register_error(self.mir.source_info(location).span, ErrorCtxt::Unexpected);
            stmts.push(vir::Stmt::Assert(vir::Assert {
                expr: vir::Expr::eq_cmp(lhs, rhs),
                position: pos,
            }));
        }

        stmts
    }

    fn encode_obtain(&mut self, expr: vir::Expr, pos: vir::Position) -> Vec<vir::Stmt> {
        let mut stmts = vec![vir::Stmt::Obtain(vir::Obtain {
            expr: expr.clone(),
            position: pos,
        })];

        if self.check_foldunfold_state {
            let new_pos = self.encoder.error_manager().duplicate_position(pos);
            self.encoder
                .error_manager()
                .set_error(new_pos, ErrorCtxt::Unexpected);
            stmts.push(vir::Stmt::Assert(vir::Assert {
                expr,
                position: new_pos,
            }));
        }

        stmts
    }

    /// A borrow is mutable if it was a MIR unique borrow, a move of
    /// a borrow, or a argument of a function.
    fn is_mutable_borrow(&self, loan: facts::Loan) -> EncodingResult<bool> {
        if let Some(stmt) = self.polonius_info().get_assignment_for_loan(loan)? {
            Ok(match stmt.kind {
                mir::StatementKind::Assign(box (_, ref rhs)) => match rhs {
                    &mir::Rvalue::Ref(_, mir::BorrowKind::Shared, _)
                    | &mir::Rvalue::Use(mir::Operand::Copy(_)) => false,
                    &mir::Rvalue::Ref(_, mir::BorrowKind::Mut { .. }, _)
                    | &mir::Rvalue::Use(mir::Operand::Move(_)) => true,
                    &mir::Rvalue::Cast(
                        mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize),
                        _,
                        _ty,
                    ) => false,
                    &mir::Rvalue::Use(mir::Operand::Constant(_)) => false,
                    x => unreachable!("{:?}", x),
                },
                ref x => unreachable!("{:?}", x),
            })
        } else {
            // It is not an assignment, so we assume that the borrow is mutable.
            Ok(true)
        }
    }

    #[tracing::instrument(level = "debug", skip_all)]
    fn construct_vir_reborrowing_dag(
        &mut self,
        loans: &[facts::Loan],
        zombie_loans: &[facts::Loan],
        location: mir::Location,
        end_location: Option<mir::Location>,
        is_in_package_stmt: bool,
    ) -> SpannedEncodingResult<vir::borrows::DAG> {
        let mir_dag = self
            .polonius_info()
            .construct_reborrowing_dag(loans, zombie_loans, location)
            .map_err(|err| self.translate_polonius_error(err))?;
        debug!(
            "construct_vir_reborrowing_dag mir_dag={}",
            mir_dag.to_string()
        );
        let mut builder = vir::borrows::DAGBuilder::new();
        for node in mir_dag.iter() {
            let node = match node.kind {
                ReborrowingKind::Assignment { loan } => self
                    .construct_vir_reborrowing_node_for_assignment(
                        &mir_dag,
                        loan,
                        node,
                        location,
                        end_location,
                        is_in_package_stmt,
                    )?,
                ReborrowingKind::Call { loan, .. } => {
                    if let Some(slice_expiry_node) =
                        self.construct_vir_reborrowing_node_for_slice(loan, node, location)?
                    {
                        slice_expiry_node
                    } else {
                        self.construct_vir_reborrowing_node_for_call(
                            &mir_dag,
                            loan,
                            node,
                            location,
                            is_in_package_stmt,
                        )?
                    }
                }
                ReborrowingKind::ArgumentMove { loan } => {
                    let loan_location = self.polonius_info().get_loan_location(&loan);
                    let guard = self.construct_location_guard(loan_location);
                    vir::borrows::Node::new(
                        guard,
                        node.loan.index().into(),
                        convert_loans_to_borrows(&node.reborrowing_loans),
                        convert_loans_to_borrows(&node.reborrowed_loans),
                        Vec::new(),
                        Vec::new(),
                        Vec::new(),
                        Vec::new(),
                        None,
                    )
                }
                ref x => unimplemented!("{:?}", x),
            };
            builder.add_node(node);
        }
        debug!(
            "construct_vir_reborrowing_dag mir_dag={}",
            mir_dag.to_string()
        );
        Ok(builder.finish())
    }

    fn construct_location_guard(&self, location: mir::Location) -> vir::Expr {
        let bbi = &location.block;
        let executed_flag_var = self.cfg_block_has_been_executed[bbi].clone();
        vir::Expr::local(executed_flag_var)
    }

    // will return None if not a slice borrow
    // as slicing is just a function call, we can only tell the difference upon
    // closer inspection
    #[tracing::instrument(level = "trace", skip(self))]
    fn construct_vir_reborrowing_node_for_slice(
        &mut self,
        loan: facts::Loan,
        node: &ReborrowingDAGNode,
        location: mir::Location,
    ) -> SpannedEncodingResult<Option<vir::borrows::Node>> {
        let span = self.mir_encoder.get_span_of_location(location);

        let loan_location = self.polonius_info().get_loan_location(&loan);
        trace!("loan_location: {:?}", loan_location);

        let loan_places = self
            .polonius_info()
            .get_loan_places(&loan)
            .map_err(EncodingError::from)
            .with_span(span)?;
        trace!("loan_places: {:?}", loan_places);

        Ok(
            if let Some(regained) = self.slice_created_at.get(&loan_location) {
                let guard = self.construct_location_guard(loan_location);
                trace!("guard: {:?}", guard);
                trace!("regained: {:?}", regained);
                Some(vir::borrows::Node::new(
                    guard,
                    node.loan.index().into(),
                    convert_loans_to_borrows(&node.reborrowing_loans),
                    convert_loans_to_borrows(&node.reborrowed_loans),
                    vec![vir::Stmt::comment("hi")],
                    vec![regained.clone()],
                    Vec::new(),
                    Vec::new(),
                    None,
                ))
            } else {
                None
            },
        )
    }

    #[tracing::instrument(level = "trace", skip(self, _mir_dag))]
    fn construct_vir_reborrowing_node_for_assignment(
        &mut self,
        _mir_dag: &ReborrowingDAG,
        loan: facts::Loan,
        node: &ReborrowingDAGNode,
        location: mir::Location,
        end_location: Option<mir::Location>,
        is_in_package_stmt: bool,
    ) -> SpannedEncodingResult<vir::borrows::Node> {
        let span = self.mir_encoder.get_span_of_location(location);
        let node_is_leaf = node.reborrowed_loans.is_empty();

        let loan_location = self.polonius_info().get_loan_location(&loan);
        let loan_places = self
            .polonius_info()
            .get_loan_places(&loan)
            .map_err(EncodingError::from)
            .with_span(span)?
            .unwrap();
        let (expiring, restored, is_mut, mut stmts) =
            self.encode_loan_places(&loan_places).with_span(span)?;
        let borrowed_places = restored.clone().into_iter().collect();
        trace!("construct_vir_reborrowing_node_for_assignment(loan={:?}, loan_places={:?}, expiring={:?}, restored={:?}, stmts={:?}", loan, loan_places, expiring, restored, stmts);

        let mut used_lhs_label = false;

        // Move the permissions from the "in loans" ("reborrowing loans") to the current loan
        if node.incoming_zombies && restored.is_some() {
            let lhs_label = self
                .get_label_after_location(loan_location)?
                .unwrap()
                .to_string();
            for &in_loan in node.reborrowing_loans.iter() {
                // TODO: Is this the correct span?
                if self.is_mutable_borrow(in_loan).with_span(span)? {
                    let in_location = self.polonius_info().get_loan_location(&in_loan);
                    let in_label = self
                        .get_label_after_location(in_location)?
                        .unwrap()
                        .to_string();
                    used_lhs_label = true;
                    stmts.extend(self.encode_transfer_permissions(
                        expiring.clone().old(in_label),
                        expiring.clone().old(lhs_label.clone()),
                        loan_location,
                        is_in_package_stmt,
                    ));
                }
            }
        }

        let lhs_place = if used_lhs_label {
            let lhs_label = self.get_label_after_location(loan_location)?.unwrap();
            expiring.old(lhs_label)
        } else {
            expiring
        };
        let rhs_place = match node.zombity {
            ReborrowingZombity::Zombie(rhs_location) if !node_is_leaf => {
                let rhs_label = self.get_label_after_location(rhs_location)?.unwrap();
                restored.map(|r| r.old(rhs_label))
            }

            _ => restored,
        };

        if is_mut {
            stmts.extend(self.encode_transfer_permissions(
                lhs_place.clone(),
                rhs_place.unwrap(),
                loan_location,
                is_in_package_stmt,
            ));
        }

        let conflicting_loans = self.polonius_info().get_conflicting_loans(node.loan);
        let deaf_location = if let Some(end_location) = end_location {
            end_location
        } else {
            location
        };
        let alive_conflicting_loans = self
            .polonius_info()
            .get_alive_conflicting_loans(node.loan, deaf_location);

        let guard = self.construct_location_guard(loan_location);

        Ok(vir::borrows::Node::new(
            guard,
            node.loan.index().into(),
            convert_loans_to_borrows(&node.reborrowing_loans),
            convert_loans_to_borrows(&node.reborrowed_loans),
            self.set_stmts_default_pos(stmts, span),
            borrowed_places,
            convert_loans_to_borrows(&conflicting_loans),
            convert_loans_to_borrows(&alive_conflicting_loans),
            Some(lhs_place),
        ))
    }

    #[tracing::instrument(level = "debug", skip_all)]
    fn construct_vir_reborrowing_node_for_call(
        &mut self,
        _mir_dag: &ReborrowingDAG,
        loan: facts::Loan,
        node: &ReborrowingDAGNode,
        location: mir::Location,
        is_in_package_stmt: bool,
    ) -> SpannedEncodingResult<vir::borrows::Node> {
        let mut stmts: Vec<vir::Stmt> = Vec::new();
        let span = self.mir_encoder.get_span_of_location(location);

        let loan_location = self.polonius_info().get_loan_location(&loan);

        // Get the borrow information.
        if !self.procedure_contracts.contains_key(&loan_location) {
            return Err(SpannedEncodingError::internal(
                format!(
                    "there is no procedure contract for loan {loan:?}. This could happen if you \
                         are chaining pure functions, which is not fully supported."
                ),
                span,
            ));
        }
        let (contract, fake_exprs) = self.procedure_contracts[&loan_location].clone();
        let replace_fake_exprs = |mut expr: vir::Expr| -> vir::Expr {
            for (fake_arg, arg_expr) in fake_exprs.iter() {
                expr = expr.replace_place(fake_arg, arg_expr);
            }
            expr
        };
        let borrow_infos = &contract.borrow_infos;
        match borrow_infos.len().cmp(&1) {
            std::cmp::Ordering::Less => (),
            std::cmp::Ordering::Greater => {
                return Err(SpannedEncodingError::internal(
                    format!(
                        "we require at most one magic wand in the postcondition. But we have {:?}",
                        borrow_infos.len()
                    ),
                    span,
                ))
            }
            std::cmp::Ordering::Equal => {
                let borrow_info = &borrow_infos[0];

                // Get the magic wand info.
                let (post_label, lhs, rhs) = self
                    .magic_wand_at_location
                    .get(&loan_location)
                    .cloned()
                    .map(|(post_label, lhs, rhs)| {
                        let lhs = self.replace_old_places_with_ghost_vars(None, lhs);
                        let rhs = self.replace_old_places_with_ghost_vars(None, rhs);
                        (post_label, lhs, rhs)
                    })
                    .unwrap();

                // Obtain the LHS permission.
                for (path, _) in &borrow_info.blocking_paths {
                    let (encoded_place, _, _) = self
                        .encode_generic_place(contract.def_id, Some(loan_location), *path)
                        .with_span(span)?;
                    let encoded_place = replace_fake_exprs(encoded_place);

                    // Move the permissions from the "in loans" ("reborrowing loans") to the current loan
                    if node.incoming_zombies {
                        for &in_loan in node.reborrowing_loans.iter() {
                            let in_location = self.polonius_info().get_loan_location(&in_loan);
                            let opt_in_label = self.get_label_after_location(in_location)?.cloned();
                            if let Some(in_label) = opt_in_label {
                                stmts.extend(self.encode_transfer_permissions(
                                    encoded_place.clone().old(in_label),
                                    encoded_place.clone().old(&post_label),
                                    loan_location,
                                    is_in_package_stmt,
                                ));
                            }
                        }
                    }
                    if !node.incoming_zombies || node.reborrowing_loans.is_empty() {
                        stmts.extend(self.encode_transfer_permissions(
                            encoded_place.clone(),
                            encoded_place.old(&post_label),
                            loan_location,
                            is_in_package_stmt,
                        ));
                    }
                }

                let pos = self.register_error(
                    //self.mir.span,
                    // TODO change to where the loan expires?
                    self.mir.source_info(loan_location).span, // the source of the ref
                    ErrorCtxt::ApplyMagicWandOnExpiry,
                );
                // Inhale the magic wand.
                let magic_wand = vir::Expr::MagicWand(vir::MagicWand {
                    left: Box::new(lhs.clone()),
                    right: Box::new(rhs.clone()),
                    borrow: Some(loan.index().into()),
                    position: pos,
                });
                stmts.push(vir::Stmt::Inhale(vir::Inhale { expr: magic_wand }));
                // Emit the apply statement.
                let statement = vir::Stmt::apply_magic_wand(lhs, rhs, loan.index().into(), pos);
                debug!("{:?} at {:?}", statement, loan_location);
                stmts.push(statement);
            }
        }

        let guard = self.construct_location_guard(loan_location);
        Ok(vir::borrows::Node::new(
            guard,
            node.loan.index().into(),
            convert_loans_to_borrows(&node.reborrowing_loans),
            convert_loans_to_borrows(&node.reborrowed_loans),
            stmts,
            Vec::new(),
            Vec::new(),
            Vec::new(),
            None,
        ))
    }

    #[tracing::instrument(level = "trace", skip(self))]
    fn encode_expiration_of_loans(
        &mut self,
        loans: Vec<facts::Loan>,
        zombie_loans: &[facts::Loan],
        location: mir::Location,
        end_location: Option<mir::Location>,
        is_in_package_stmt: bool,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        let mut stmts: Vec<vir::Stmt> = vec![];
        if !loans.is_empty() {
            let vir_reborrowing_dag = self.construct_vir_reborrowing_dag(
                &loans,
                zombie_loans,
                location,
                end_location,
                is_in_package_stmt,
            )?;
            stmts.push(vir::Stmt::ExpireBorrows(vir::ExpireBorrows {
                dag: vir_reborrowing_dag,
            }));
        }
        Ok(stmts)
    }

    #[tracing::instrument(level = "debug", skip(self))]
    fn encode_expiring_borrows_between(
        &mut self,
        begin_loc: mir::Location,
        end_loc: mir::Location,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        let (all_dying_loans, zombie_loans) = self
            .polonius_info()
            .get_all_loans_dying_between(begin_loc, end_loc);
        // FIXME: is 'end_loc' correct here? What about 'begin_loc'?
        self.encode_expiration_of_loans(
            all_dying_loans,
            &zombie_loans,
            begin_loc,
            Some(end_loc),
            false,
        )
    }

    #[tracing::instrument(level = "debug", skip(self))]
    fn encode_expiring_borrows_at(
        &mut self,
        location: mir::Location,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        let (all_dying_loans, zombie_loans) = self.polonius_info().get_all_loans_dying_at(location);
        let stmts =
            self.encode_expiration_of_loans(all_dying_loans, &zombie_loans, location, None, false)?;
        Ok(self.set_stmts_default_pos(stmts, self.mir_encoder.get_span_of_location(location)))
    }

    /// Note: it's better to call `encode_statement_at` instead of this method.
    #[tracing::instrument(level = "debug", skip(self), fields(terminator = ?term.kind, span = ?term.source_info.span))]
    fn encode_terminator(
        &mut self,
        term: &mir::Terminator<'tcx>,
        location: mir::Location,
    ) -> SpannedEncodingResult<(Vec<vir::Stmt>, MirSuccessor)> {
        let mut stmts: Vec<vir::Stmt> = vec![vir::Stmt::comment(format!("[mir] {:?}", term.kind))];
        let span = self.mir_encoder.get_span_of_location(location);

        let result = match term.kind {
            TerminatorKind::Return => {
                // Package magic wands, if there is any
                let postcondition_label = self.cfg_method.get_fresh_label_name();
                stmts.extend(self.encode_package_end_of_method(
                    PRECONDITION_LABEL,
                    &postcondition_label,
                    location,
                )?);

                (stmts, MirSuccessor::Return)
            }

            TerminatorKind::Goto { target } => (stmts, MirSuccessor::Goto(target)),

            TerminatorKind::SwitchInt {
                ref discr,
                ref targets,
            } => {
                let switch_ty = self.mir_encoder.get_operand_ty(discr);
                trace!(
                    "SwitchInt ty '{:?}', discr '{:?}', targets '{:?}'",
                    switch_ty,
                    discr,
                    targets
                );

                {
                    // Check whether we should not omit the spec block.
                    let all_targets = targets.all_targets();
                    if all_targets.len() == 2 {
                        if let Some(spec) = all_targets
                            .iter()
                            .position(|target| self.procedure.is_spec_block(*target))
                        {
                            let real_target = all_targets[(spec + 1) % 2];
                            let spec_target = all_targets[spec];
                            if let Some(statements) = self.specification_block_encoding.remove(&spec_target) && !statements.is_empty()
                            {
                                stmts.push(
                                    vir::Stmt::comment(
                                        format!("Specification from block: {spec_target:?}")
                                    )
                                );
                                stmts.extend(statements);
                                return Ok((stmts, MirSuccessor::Goto(
                                    real_target
                                )));
                            }
                        }
                    }
                }

                let mut cfg_targets: Vec<(vir::Expr, BasicBlockIndex)> = vec![];

                // Use a local variable for the discriminant.
                // See Silicon issue https://github.com/viperproject/silicon/issues/356
                let discr_var = match switch_ty.kind() {
                    ty::TyKind::Bool => self.cfg_method.add_fresh_local_var(vir::Type::Bool),

                    ty::TyKind::Int(_) | ty::TyKind::Uint(_) | ty::TyKind::Char => {
                        self.cfg_method.add_fresh_local_var(vir::Type::Int)
                    }

                    ty::TyKind::Float(ty::FloatTy::F32) => self
                        .cfg_method
                        .add_fresh_local_var(vir::Type::Float(Float::F32)),

                    ty::TyKind::Float(ty::FloatTy::F64) => self
                        .cfg_method
                        .add_fresh_local_var(vir::Type::Float(Float::F64)),

                    ref x => unreachable!("{:?}", x),
                };
                let encoded_discr = self
                    .mir_encoder
                    .encode_operand_expr(discr)
                    .with_span(span)?;
                stmts.push(vir::Stmt::Assign(vir::Assign {
                    target: discr_var.clone().into(),
                    source: encoded_discr,
                    kind: vir::AssignKind::Copy,
                }));

                let guard_is_bool = matches!(switch_ty.kind(), ty::TyKind::Bool);

                for (value, target) in targets.iter() {
                    // Convert int to bool, if required
                    let viper_guard = match switch_ty.kind() {
                        ty::TyKind::Bool => {
                            if value == 0 {
                                // If discr is 0 (false)
                                vir::Expr::not(discr_var.clone().into())
                            } else {
                                // If discr is not 0 (true)
                                discr_var.clone().into()
                            }
                        }

                        ty::TyKind::Int(_) | ty::TyKind::Uint(_) | ty::TyKind::Char => {
                            vir::Expr::eq_cmp(
                                discr_var.clone().into(),
                                self.encoder.encode_int_cast(value, switch_ty),
                            )
                        }

                        ref x => unreachable!("{:?}", x),
                    };
                    cfg_targets.push((viper_guard, target))
                }
                let mut default_target = targets.otherwise();
                let mut kill_default_target = false;

                // Is the target an unreachable block?
                if let mir::TerminatorKind::Unreachable = self.mir[default_target].terminator().kind
                {
                    stmts.push(vir::Stmt::comment(format!(
                        "Ignore default target {default_target:?}, as the compiler marked it as unreachable."
                    )));
                    kill_default_target = true;
                };

                // Is the target a specification block?
                if self.procedure.is_spec_block(default_target) {
                    stmts.push(vir::Stmt::comment(format!(
                        "Ignore default target {default_target:?}, as it is only used by Prusti to type-check \
                        a loop invariant."
                    )));
                    kill_default_target = true;
                };

                if kill_default_target {
                    // Use the last conditional target as default. We could also assume or assert
                    // that the switch is exhaustive and never hits the default.
                    let last_target = cfg_targets.pop().unwrap();
                    (stmts, MirSuccessor::GotoSwitch(cfg_targets, last_target.1))
                } else {
                    // Reorder the targets such that Silicon explores branches in the order that we want
                    if guard_is_bool && cfg_targets.len() == 1 {
                        let (target_guard, target) = cfg_targets.pop().unwrap();
                        let target_span = self.mir_encoder.get_span_of_basic_block(target);
                        let default_target_span =
                            self.mir_encoder.get_span_of_basic_block(default_target);
                        if target_span > default_target_span {
                            let guard_pos = target_guard.pos();
                            cfg_targets =
                                vec![(target_guard.negate().set_pos(guard_pos), default_target)];
                            default_target = target;
                        } else {
                            // Undo the pop
                            cfg_targets.push((target_guard, target));
                        }
                    }
                    (stmts, MirSuccessor::GotoSwitch(cfg_targets, default_target))
                }
            }

            TerminatorKind::Unreachable => {
                // Asserting `false` here does not work. See issue #158
                //let pos = self.register_error(
                //    term.source_info.span,
                //    ErrorCtxt::UnreachableTerminator
                //);
                //stmts.push(
                //    vir::Stmt::Inhale(false.into())
                //);
                (stmts, MirSuccessor::Kill)
            }

            TerminatorKind::UnwindTerminate(..) => {
                let pos = self.register_error(term.source_info.span, ErrorCtxt::AbortTerminator);
                stmts.push(vir::Stmt::Assert(vir::Assert {
                    expr: false.into(),
                    position: pos,
                }));
                (stmts, MirSuccessor::Kill)
            }

            TerminatorKind::Drop { target, .. } => (stmts, MirSuccessor::Goto(target)),

            TerminatorKind::FalseEdge { real_target, .. } => {
                (stmts, MirSuccessor::Goto(real_target))
            }

            TerminatorKind::FalseUnwind { real_target, .. } => {
                (stmts, MirSuccessor::Goto(real_target))
            }

            TerminatorKind::Call {
                ref args,
                destination,
                target,
                func: mir::Operand::Constant(box mir::Constant { literal, .. }),
                ..
            } => {
                let ty = literal.ty();
                let func_const_val = literal.try_to_scalar_int();
                if let ty::TyKind::FnDef(called_def_id, call_substs) = ty.kind() {
                    let called_def_id = *called_def_id;
                    debug!(
                        "Encode function call {:?} with substs {:?}",
                        called_def_id, call_substs
                    );

                    let full_func_proc_name: &str = &self
                        .encoder
                        .env()
                        .name
                        .get_absolute_item_name(called_def_id);

                    match full_func_proc_name {
                        "std::rt::begin_panic"
                        | "core::panicking::panic"
                        | "core::panicking::panic_fmt" => {
                            // This is called when a Rust assertion fails
                            // args[0]: message
                            // args[1]: position of failing assertions

                            // Example of args[0]: 'const "internal error: entered unreachable code"'
                            let panic_message = format!("{:?}", args[0]);

                            let panic_cause =
                                self.mir_encoder.encode_panic_cause(term.source_info.span);
                            let pos = self.register_error(
                                term.source_info.span,
                                ErrorCtxt::Panic(panic_cause),
                            );

                            if self.check_panics {
                                stmts.push(vir::Stmt::comment(format!(
                                    "Rust panic - {panic_message}"
                                )));
                                stmts.push(vir::Stmt::Assert(vir::Assert {
                                    expr: false.into(),
                                    position: pos,
                                }));
                            } else {
                                debug!("Absence of panic will not be checked")
                            }
                        }

                        "std::boxed::Box::<T>::new" | "alloc::boxed::Box::<T>::new" => {
                            // This is the initialization of a box
                            // args[0]: value to put in the box
                            assert_eq!(args.len(), 1);

                            let (dst, pre_stmts, dest_ty, _) =
                                self.encode_place(destination, ArrayAccessKind::Shared, location)?;
                            stmts.extend(pre_stmts);

                            let boxed_ty = dest_ty.boxed_ty();
                            let ref_field = self
                                .encoder
                                .encode_dereference_field(boxed_ty)
                                .with_span(span)?;

                            let box_content = dst.clone().field(ref_field.clone());

                            stmts.extend(self.prepare_assign_target(
                                dst,
                                ref_field,
                                location,
                                vir::AssignKind::Move,
                                false,
                            )?);

                            // Allocate `box_content`
                            stmts.extend(
                                self.encode_havoc_and_initialization(&box_content)
                                    .with_span(span)?,
                            );

                            // Initialize `box_content`
                            stmts.extend(self.encode_assign_operand(
                                &box_content,
                                &args[0],
                                location,
                            )?);
                        }

                        "std::cmp::PartialEq::eq" | "core::cmp::PartialEq::eq"
                            if args.len() == 2
                                && self.encoder.has_structural_eq_impl(
                                    self.mir_encoder.get_operand_ty(&args[0]),
                                ) =>
                        {
                            debug!("Encoding call of PartialEq::eq");
                            stmts.extend(self.encode_cmp_function_call(
                                called_def_id,
                                location,
                                term.source_info.span,
                                args,
                                destination,
                                target,
                                vir::BinaryOpKind::EqCmp,
                                call_substs,
                            )?);
                        }

                        "std::cmp::PartialEq::ne" | "core::cmp::PartialEq::ne"
                            if args.len() == 2
                                && self.encoder.has_structural_eq_impl(
                                    self.mir_encoder.get_operand_ty(&args[0]),
                                ) =>
                        {
                            debug!("Encoding call of PartialEq::ne");
                            stmts.extend(self.encode_cmp_function_call(
                                called_def_id,
                                location,
                                term.source_info.span,
                                args,
                                destination,
                                target,
                                vir::BinaryOpKind::NeCmp,
                                call_substs,
                            )?);
                        }

                        "std::ops::Fn::call" | "core::ops::Fn::call" => {
                            let cl_type: ty::Ty = call_substs[0].expect_ty();
                            match cl_type.kind() {
                                ty::TyKind::Closure(cl_def_id, _) => {
                                    debug!(
                                        "Encoding call to closure {:?} with func {:?}",
                                        cl_def_id, func_const_val
                                    );
                                    stmts.extend(self.encode_impure_function_call(
                                        location,
                                        term.source_info.span,
                                        args,
                                        destination,
                                        target,
                                        *cl_def_id,
                                        call_substs,
                                    )?);
                                }

                                _ => {
                                    return Err(SpannedEncodingError::unsupported(
                                        format!("only calls to closures are supported. The term is a {:?}, not a closure.", cl_type.kind()),
                                        term.source_info.span,
                                    ));
                                }
                            }
                        }

                        "core::slice::<impl [T]>::len" => {
                            stmts.extend(self.encode_slice_len_call(
                                destination,
                                args,
                                location,
                                span,
                            )?);
                        }

                        "std::iter::Iterator::next" | "core::iter::Iterator::next" => {
                            return Err(SpannedEncodingError::unsupported(
                                "iterators are not fully supported yet",
                                term.source_info.span,
                            ));
                        }

                        // TODO: use extern_spec
                        "core::ops::IndexMut::index_mut" | "std::ops::IndexMut::index_mut" => {
                            return Err(SpannedEncodingError::unsupported(
                                "mutably slicing is not fully supported yet",
                                term.source_info.span,
                            ));
                        }

                        "core::ops::Index::index" | "std::ops::Index::index" => {
                            stmts.extend(
                                self.encode_sequence_index_call(
                                    destination,
                                    args,
                                    location,
                                    term.source_info.span,
                                )
                                .with_span(span)?,
                            );
                        }

                        _ => {
                            // The called method might be a trait method.
                            // We try to resolve it to the concrete implementation
                            // and type substitutions.
                            let (called_def_id, call_substs) = self
                                .encoder
                                .env()
                                .query
                                .resolve_method_call(self.proc_def_id, called_def_id, call_substs);

                            let is_pure_function = self.encoder.is_pure(called_def_id, Some(call_substs)) &&
                                // We are verifying this pure function and,
                                // therefore, need to always encode it as a
                                // method.
                                self.proc_def_id != called_def_id;
                            if is_pure_function {
                                let def_id = called_def_id;
                                let (function_name, _) = self
                                    .encoder
                                    .encode_pure_function_use(def_id, self.proc_def_id, call_substs)
                                    .with_default_span(term.source_info.span)?;
                                debug!("Encoding pure function call '{}'", function_name);
                                assert!(target.is_some());
                                for operand in args.iter() {
                                    // Check that the operand's type is Copy
                                    let _ = self.mir_encoder.encode_operand_expr(operand);
                                }

                                stmts.extend(self.encode_pure_function_call(
                                    location,
                                    term.source_info.span,
                                    args,
                                    destination,
                                    target,
                                    def_id,
                                    call_substs,
                                )?);
                            } else {
                                stmts.extend(self.encode_impure_function_call(
                                    location,
                                    term.source_info.span,
                                    args,
                                    destination,
                                    target,
                                    called_def_id,
                                    call_substs,
                                )?);
                            }
                        }
                    }

                    if let Some(target) = target {
                        (stmts, MirSuccessor::Goto(target))
                    } else {
                        // Encode unreachability
                        //stmts.push(
                        //    vir::Stmt::Inhale(false.into())
                        //);
                        (stmts, MirSuccessor::Kill)
                    }
                } else {
                    // Other kind of calls?
                    unimplemented!();
                }
            }

            TerminatorKind::Call { .. } => {
                // Other kind of calls?
                unimplemented!();
            }

            TerminatorKind::Assert {
                ref cond,
                expected,
                target,
                ref msg,
                ..
            } => {
                trace!("Assert cond '{:?}', expected '{:?}'", cond, expected);

                // Use local variables in the switch/if.
                // See Silicon issue https://github.com/viperproject/silicon/issues/356
                let cond_var = self.cfg_method.add_fresh_local_var(vir::Type::Bool);
                stmts.push(vir::Stmt::Assign(vir::Assign {
                    target: cond_var.clone().into(),
                    source: self
                        .mir_encoder
                        .encode_operand_expr(cond)
                        .with_span(self.mir_encoder.get_span_of_location(location))?,
                    kind: vir::AssignKind::Copy,
                }));

                let viper_guard = if expected {
                    cond_var.into()
                } else {
                    vir::Expr::not(cond_var.into())
                };

                // Check or assume the assertion
                let (assert_msg, error_ctxt) = if let box mir::AssertKind::BoundsCheck { .. } = msg
                {
                    let mut s = String::new();
                    msg.fmt_assert_args(&mut s).unwrap();
                    (s, ErrorCtxt::BoundsCheckAssert)
                } else {
                    let assert_msg = msg.description().to_string();
                    (assert_msg.clone(), ErrorCtxt::AssertTerminator(assert_msg))
                };

                stmts.push(vir::Stmt::comment(format!("Rust assertion: {assert_msg}")));
                if self.check_panics {
                    stmts.push(vir::Stmt::Assert(vir::Assert {
                        expr: viper_guard,
                        position: self.register_error(term.source_info.span, error_ctxt),
                    }));
                } else {
                    stmts.push(vir::Stmt::comment("This assertion will not be checked"));
                    stmts.push(vir::Stmt::Inhale(vir::Inhale { expr: viper_guard }));
                };

                (stmts, MirSuccessor::Goto(target))
            }

            TerminatorKind::UnwindResume
            | TerminatorKind::Yield { .. }
            | TerminatorKind::GeneratorDrop
            | TerminatorKind::InlineAsm { .. } => unimplemented!("{:?}", term.kind),
        };
        Ok(result)
    }

    #[tracing::instrument(level = "debug", skip(self))]
    fn encode_slice_len_call(
        &mut self,
        destination: mir::Place<'tcx>,
        args: &[mir::Operand<'tcx>],
        location: mir::Location,
        span: Span,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        assert!(args.len() == 1, "unexpected args to slice::len(): {args:?}");
        let slice_operand = self
            .mir_encoder
            .encode_operand_expr(&args[0])
            .with_span(span)?;

        let mut stmts = vec![];

        // we need to put a label before, it seems..
        let label = self.cfg_method.get_fresh_label_name();
        stmts.push(vir::Stmt::label(label.clone()));

        let slice_ty_ref = self.mir_encoder.get_operand_ty(&args[0]);
        let slice_ty = if let ty::TyKind::Ref(_, slice_ty, _) = slice_ty_ref.kind() {
            slice_ty
        } else {
            unreachable!()
        };
        let slice_types = self
            .encoder
            .encode_sequence_types(*slice_ty)
            .with_span(span)?;

        let rhs = slice_types.len(self.encoder, slice_operand);

        let (encoded_lhs, encode_stmts, ty, _) = self
            .encode_place(
                destination,
                ArrayAccessKind::Mutable(None, location),
                location,
            )
            .with_span(span)?;
        stmts.extend(encode_stmts);

        stmts.extend(self.encode_copy_value_assign(encoded_lhs, rhs, ty, location)?);

        self.encode_transfer_args_permissions(location, args, &mut stmts, &label, false)?;

        // Store a label for permissions got back from the call
        debug!(
            "Pure function call location {:?} has label {}",
            location, label
        );
        self.label_after_location.insert(location, label);

        Ok(stmts)
    }

    #[tracing::instrument(level = "debug", skip(self))]
    fn encode_sequence_index_call(
        &mut self,
        destination: mir::Place<'tcx>,
        args: &[mir::Operand<'tcx>],
        location: mir::Location,
        error_span: Span,
    ) -> EncodingResult<Vec<vir::Stmt>> {
        // args[0] is the base array/slice, args[1] is the index
        // index is not specified exactly, as std::ops::Index::index is a trait method, so all we
        // know is there needs to be an impl Index<Idx> for T
        assert!(
            args.len() == 2,
            "unexpected args to sequence index call: {args:?}"
        );

        let mut stmts = vec![];

        // we need to put a label before, it seems..
        let label = self.cfg_method.get_fresh_label_name();
        stmts.push(vir::Stmt::label(label.clone()));

        let loan = self.polonius_info().get_loan_at_location(location);
        let (encoded_lhs, encode_stmts, lhs_ty, _) = self.encode_place(
            destination,
            ArrayAccessKind::Mutable(Some(loan.index().into()), location),
            location,
        )?;
        stmts.extend(encode_stmts);
        if !lhs_ty.is_slice_or_ref() && !lhs_ty.is_array_or_ref() {
            error_unsupported!("Non-slice LHS type '{:?}' not supported yet", lhs_ty);
        }
        let mutability = if let ty::TyKind::Ref(_, _, mutability) = lhs_ty.kind() {
            mutability
        } else {
            unreachable!()
        };
        let perm_amount = match mutability {
            Mutability::Mut => vir::PermAmount::Write,
            Mutability::Not => vir::PermAmount::Read,
        };

        stmts.extend(self.encode_havoc(&encoded_lhs)?);
        stmts.push(vir_stmt!{ inhale [vir::Expr::pred_permission(encoded_lhs.clone(), perm_amount).unwrap()] });

        let lhs_slice_ty = lhs_ty.peel_refs();
        let lhs_slice_expr = self
            .encoder
            .encode_value_expr(encoded_lhs.clone(), lhs_ty)?;

        let base_seq = self.mir_encoder.encode_operand_place(&args[0])?.unwrap();
        let base_seq_ty = self.mir_encoder.get_operand_ty(&args[0]);

        if !base_seq_ty.is_slice_or_ref() && !base_seq_ty.is_array_or_ref() {
            error_unsupported!(
                "Slicing is only supported for arrays/slices currently, not '{:?}'",
                base_seq_ty
            );
        }

        // base_seq is expected to be ref$Array$.. or ref$Slice$.., but lookup_pure wants the
        // contained Array$../Slice$..
        let base_seq_expr = self.encoder.encode_value_expr(base_seq, base_seq_ty)?;

        let enc_sequence_types = self
            .encoder
            .encode_sequence_types(base_seq_ty.peel_refs())?;

        let j = vir_local! { j: Int };
        let elem_snap_ty = self
            .encoder
            .encode_snapshot_type(enc_sequence_types.elem_ty_rs)?;
        let rhs_lookup_j = enc_sequence_types.encode_lookup_pure_call(
            self.encoder,
            base_seq_expr.clone(),
            j.clone().into(),
            elem_snap_ty,
        );

        let encoded_idx = self.mir_encoder.encode_operand_place(&args[1])?.unwrap();
        trace!("idx: {:?}", encoded_idx);
        let idx_ty = self.mir_encoder.get_operand_ty(&args[1]);
        let idx_ident = self
            .encoder
            .env()
            .name
            .get_absolute_item_name(idx_ty.ty_adt_def().unwrap().did());
        trace!("ident: {}", idx_ident);

        self.slice_created_at.insert(location, encoded_lhs);

        let original_len = enc_sequence_types.len(self.encoder, base_seq_expr);

        // TODO: there's fields like _5.f$start.val_int on `encoded_idx`, it just feels hacky to
        // manually re-do and hardcode them here when we probably just encoded the type
        // and the construction of the fields.
        let usize_ty = self
            .encoder
            .env()
            .tcx()
            .mk_ty_from_kind(ty::TyKind::Uint(ty::UintTy::Usize));
        let start = match &*idx_ident {
            "std::ops::Range"
            | "core::ops::Range"
            | "std::ops::RangeFrom"
            | "core::ops::RangeFrom" => {
                let start_expr = self.encoder.encode_struct_field_value(
                    encoded_idx.clone(),
                    "start",
                    usize_ty,
                )?;
                if self.check_panics {
                    // Check indexing in bounds
                    stmts.push(vir::Stmt::Assert(vir::Assert {
                        expr: vir_expr! { [start_expr] >= [vir::Expr::from(0usize)] },
                        position: self.register_error(
                            error_span,
                            ErrorCtxt::SliceRangeBoundsCheckAssert(
                                "the range start value may be smaller than 0 when slicing"
                                    .to_string(),
                            ),
                        ),
                    }));
                }
                start_expr
            }
            // RangeInclusive is wierdly differnet to all of the other Range*s in that the struct fields are private
            // and it is created with a new() fn and start/end are accessed with getter fns
            // See https://github.com/rust-lang/rust/issues/67371 for why this is the case...
            "std::ops::RangeInclusive" | "core::ops::RangeInclusive" => {
                return Err(EncodingError::unsupported(
                    "slicing with RangeInclusive (e.g. [x..=y]) currently not supported"
                        .to_string(),
                ))
            }
            "std::ops::RangeTo"
            | "core::ops::RangeTo"
            | "std::ops::RangeFull"
            | "core::ops::RangeFull"
            | "std::ops::RangeToInclusive"
            | "core::ops::RangeToInclusive" => vir::Expr::from(0usize),
            _ => unreachable!("{}", idx_ident),
        };
        let end = match &*idx_ident {
            "std::ops::Range" | "core::ops::Range" | "std::ops::RangeTo" | "core::ops::RangeTo" => {
                let end_expr =
                    self.encoder
                        .encode_struct_field_value(encoded_idx, "end", usize_ty)?;
                if self.check_panics {
                    // Check indexing in bounds
                    stmts.push(vir::Stmt::Assert(vir::Assert {
                        expr: vir_expr! { [end_expr] <= [original_len] },
                        position: self.register_error(
                            error_span,
                            ErrorCtxt::SliceRangeBoundsCheckAssert(
                                "the range end value may be out of bounds when slicing".to_string(),
                            ),
                        ),
                    }));
                }
                end_expr
            }
            "std::ops::RangeInclusive" | "core::ops::RangeInclusive" => {
                return Err(EncodingError::unsupported(
                    "slicing with RangeInclusive (e.g. [x..=y]) currently not supported"
                        .to_string(),
                ))
            }
            "std::ops::RangeToInclusive" | "core::ops::RangeToInclusive" => {
                let end_expr =
                    self.encoder
                        .encode_struct_field_value(encoded_idx, "end", usize_ty)?;
                let end_expr = vir_expr! { [end_expr] + [vir::Expr::from(1usize)] };
                if self.check_panics {
                    // Check indexing in bounds
                    stmts.push(vir::Stmt::Assert(vir::Assert {
                        expr: vir_expr! { [end_expr] <= [original_len] },
                        position: self.register_error(
                            error_span,
                            ErrorCtxt::SliceRangeBoundsCheckAssert(
                                "the range end value may be out of bounds when slicing".to_string(),
                            ),
                        ),
                    }));
                }
                end_expr
            }
            "std::ops::RangeFrom"
            | "core::ops::RangeFrom"
            | "std::ops::RangeFull"
            | "core::ops::RangeFull" => original_len,
            _ => unreachable!("{}", idx_ident),
        };

        trace!("start: {}, end: {}", start, end);

        let slice_types_lhs = self.encoder.encode_sequence_types(lhs_slice_ty)?;
        let elem_snap_ty = self
            .encoder
            .encode_snapshot_type(slice_types_lhs.elem_ty_rs)?;

        // length
        let length = vir_expr! { [end] - [start] };
        if self.check_panics {
            // start must be leq than end
            if idx_ident != "std::ops::RangeFull" && idx_ident != "core::ops::RangeFull" {
                stmts.push(vir::Stmt::Assert(vir::Assert {
                    expr: vir_expr! { [start] <= [end] },
                    position: self.register_error(
                        error_span,
                        ErrorCtxt::SliceRangeBoundsCheckAssert(
                            "the range end may be smaller than the start when slicing".to_string(),
                        ),
                    ),
                }));
            }
        }

        let slice_len_call = slice_types_lhs.len(self.encoder, lhs_slice_expr.clone());
        stmts.push(vir_stmt! {
            inhale [vir_expr!{ [slice_len_call] == [length] }]
        });

        // lookup_pure: contents
        let i = vir_local! { i: Int };
        let i_var: vir::Expr = i.clone().into();
        let j_var: vir::Expr = j.clone().into();

        let lhs_lookup_i = {
            slice_types_lhs.encode_lookup_pure_call(
                self.encoder,
                lhs_slice_expr,
                i_var.clone(),
                elem_snap_ty,
            )
        };

        // NOTE: the lhs_ and rhs_ here refer to the moment the slice is created, so lhs_lookup is
        // lookup on the slice currently being created, and rhs_lookup is on the array or slice
        // being sliced
        let lookup_eq = vir_expr! { [lhs_lookup_i] == [rhs_lookup_j] };
        let indices = vir_expr! {
            [vir_expr!{ [vir::Expr::from(0usize)] <= [i_var] }] &&
            (
                [vir_expr!{ [i_var] < [slice_len_call] }] &&
                (
                    [vir_expr!{ [j_var] == [vir_expr!{ [i_var] + [start] }] }] &&
                    (
                        [vir_expr!{ [start] <= [j_var] }] &&
                        [vir_expr!{ [j_var] < [end] }]
                    )
                )
            )
        };

        // forall i: Int, j: Int :: { lhs_lookup(i), rhs_lookup(j) } 0 <= i && i < slice$len && j == i + start && start <= j && j < end ==> lhs_lookup(i) == rhs_lookup(j)
        stmts.push(vir_stmt! {
            inhale [
                vir::Expr::forall(
                    vec![i, j],
                    vec![vir::Trigger::new(vec![lhs_lookup_i, rhs_lookup_j])],
                    vir_expr!{ ([indices] ==> [lookup_eq]) }
                )
            ]
        });

        self.encode_transfer_args_permissions(location, args, &mut stmts, &label, false)?;
        // Store a label for permissions got back from the call
        debug!(
            "Pure function call location {:?} has label {}",
            location, label
        );
        self.label_after_location.insert(location, label);

        // plan
        //
        // [x] inhale Array$lookup_pure == Slice$lookup_pure with quantifier from start to end
        // [?] label, encode_transfer_permissions?
        // [ ] what if the index is not a range? should support Index<usize> for arrays and slices maybe, mostly implemented anyway i guess

        Ok(stmts)
    }

    #[allow(clippy::too_many_arguments)]
    fn encode_cmp_function_call(
        &mut self,
        called_def_id: ProcedureDefId,
        location: mir::Location,
        call_site_span: Span,
        args: &[mir::Operand<'tcx>],
        destination: mir::Place<'tcx>,
        target: Option<BasicBlockIndex>,
        bin_op: vir::BinaryOpKind,
        substs: ty::GenericArgsRef<'tcx>,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        let arg_ty = self.mir_encoder.get_operand_ty(&args[0]);

        if self
            .encoder
            .supports_snapshot_equality(arg_ty)
            .with_span(call_site_span)?
        {
            let lhs = self
                .mir_encoder
                .encode_operand_expr(&args[0])
                .with_span(call_site_span)?;
            let rhs = self
                .mir_encoder
                .encode_operand_expr(&args[1])
                .with_span(call_site_span)?;

            let expr = match bin_op {
                vir::BinaryOpKind::EqCmp => {
                    vir::Expr::eq_cmp(vir::Expr::snap_app(lhs), vir::Expr::snap_app(rhs))
                }
                vir::BinaryOpKind::NeCmp => {
                    vir::Expr::ne_cmp(vir::Expr::snap_app(lhs), vir::Expr::snap_app(rhs))
                }
                _ => unreachable!(),
            };

            let (target_value, mut stmts) = self
                .encode_pure_function_call_lhs_value(destination, target, location)
                .with_span(call_site_span)?;
            let inhaled_expr = vir::Expr::eq_cmp(target_value, expr);

            let (call_stmts, label) =
                self.encode_pure_function_call_site(location, destination, target, inhaled_expr)?;
            stmts.extend(call_stmts);

            self.encode_transfer_args_permissions(location, args, &mut stmts, &label, false)?;

            Ok(stmts)
        } else {
            // the equality check involves some unsupported feature;
            // treat it as any other function
            self.encode_impure_function_call(
                location,
                call_site_span,
                args,
                destination,
                target,
                called_def_id,
                substs,
            )
        }
    }

    /// Encode an edge of the MIR graph
    fn encode_edge_block(
        &mut self,
        source: BasicBlockIndex,
        destination: BasicBlockIndex,
        force_block: bool,
    ) -> SpannedEncodingResult<Option<CfgBlockIndex>> {
        let source_loc = mir::Location {
            block: source,
            statement_index: self.mir[source].statements.len(),
        };
        let destination_loc = mir::Location {
            block: destination,
            statement_index: 0,
        };
        let stmts = self.encode_expiring_borrows_between(source_loc, destination_loc)?;

        if force_block || !stmts.is_empty() {
            let edge_label = self.cfg_method.get_fresh_label_name();
            let edge_block = self.cfg_method.add_block(
                &edge_label,
                vec![
                    vir::Stmt::comment(format!("========== {edge_label} ==========")),
                    vir::Stmt::comment(format!("MIR edge {source:?} --> {destination:?}")),
                ],
            );
            if !stmts.is_empty() {
                self.cfg_method
                    .add_stmt(edge_block, vir::Stmt::comment("Expire borrows"));
                self.cfg_method.add_stmts(edge_block, stmts);
            }
            Ok(Some(edge_block))
        } else {
            Ok(None)
        }
    }

    #[allow(clippy::too_many_arguments)]
    #[tracing::instrument(level = "debug", skip(self))]
    fn encode_impure_function_call(
        &mut self,
        location: mir::Location,
        call_site_span: prusti_rustc_interface::span::Span,
        mir_args: &[mir::Operand<'tcx>],
        destination: mir::Place<'tcx>,
        target: Option<BasicBlockIndex>,
        called_def_id: ProcedureDefId,
        mut substs: ty::GenericArgsRef<'tcx>,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        let full_func_proc_name = &self
            .encoder
            .env()
            .name
            .get_absolute_item_name(called_def_id);
        debug!(
            "Encoding non-pure function call '{}' with args {:?} and substs {:?}",
            full_func_proc_name, mir_args, substs
        );

        // Spans for fake exprs that cannot be encoded in viper
        let mut fake_expr_spans: FxHashMap<Local, Span> = FxHashMap::default();

        // First we construct the "operands" vector. This construction differs
        // for closure calls, where we need to unpack a tuple into the actual
        // call arguments. The components of the operands tuples are:
        // - the original MIR Operand
        // - the VIR Local that will hold hold the argument before the call
        // - the type of the argument
        // - if not constant, the VIR expression for the argument
        let mut operands: Vec<(&mir::Operand<'tcx>, Local, ty::Ty<'tcx>, Option<vir::Expr>)> =
            vec![];
        let mut encoded_operands = mir_args
            .iter()
            .map(|arg| self.mir_encoder.encode_operand_place(arg))
            .collect::<Result<Vec<Option<vir::Expr>>, _>>()
            .with_span(call_site_span)?;
        if self.encoder.env().query.is_closure(called_def_id) {
            // Closure calls are wrapped around std::ops::Fn::call(), which receives
            // two arguments: The closure instance, and the tupled-up arguments
            assert_eq!(mir_args.len(), 2);

            let cl_ty = self.mir_encoder.get_operand_ty(&mir_args[0]);
            operands.push((
                &mir_args[0],
                mir_args[0]
                    .place()
                    .and_then(|place| place.as_local())
                    .map_or_else(|| self.locals.get_fresh(cl_ty), |local| local.into()),
                cl_ty,
                encoded_operands[0].take(),
            ));

            let arg_tuple_ty = self.mir_encoder.get_operand_ty(&mir_args[1]);
            if let ty::TyKind::Tuple(arg_types) = arg_tuple_ty.kind() {
                for (field_num, arg_ty) in arg_types.into_iter().enumerate() {
                    let arg = self.locals.get_fresh(arg_ty);
                    fake_expr_spans.insert(arg, call_site_span);
                    let value_field = self
                        .encoder
                        .encode_raw_ref_field(format!("tuple_{field_num}"), arg_ty)
                        .with_span(call_site_span)?;
                    operands.push((
                        &mir_args[1], // not actually used ...
                        arg,
                        arg_ty,
                        Some(encoded_operands[1].take().unwrap().field(value_field)),
                    ));
                }
            } else {
                unimplemented!();
            }

            // TODO: weird fix for closure call substitutions, we need to
            // prepend the identity substs of the containing method ...
            substs = self
                .encoder
                .env()
                .tcx()
                .mk_args_from_iter(self.substs.iter().chain(substs));
        } else {
            for (arg, encoded_operand) in mir_args.iter().zip(encoded_operands.iter_mut()) {
                let arg_ty = self.mir_encoder.get_operand_ty(arg);
                operands.push((
                    arg,
                    arg.place()
                        .and_then(|place| place.as_local())
                        .map_or_else(|| self.locals.get_fresh(arg_ty), |local| local.into()),
                    arg_ty,
                    encoded_operand.take(),
                ));
            }
        };

        // Arguments can be places or constants. For constants, we pretend they're places by
        // creating a new local variable of the same type. For arguments that are not just local
        // variables (i.e., for places that have projections), we do the same. We don't replace
        // arguments that are just local variables with a new local variable.
        // This data structure maps the newly created local variables to the expression that was
        // originally passed as an argument.
        let mut fake_exprs: FxHashMap<vir::Expr, vir::Expr> = FxHashMap::default();

        let mut arguments = vec![];

        let mut const_arg_vars: FxHashSet<vir::Expr> = FxHashSet::default();
        let mut type_invs: Vec<vir::Expr> = vec![];
        let mut constant_args = vec![];

        let mut stmts = vec![];
        let mut stmts_after: Vec<vir::Stmt> = vec![];

        for (mir_arg, arg, arg_ty, encoded_operand) in operands {
            arguments.push(arg);

            let encoded_local = self.encode_prusti_local(arg);
            let arg_place = vir::Expr::local(encoded_local);
            debug!("arg: {:?} {}", arg, arg_place);

            match encoded_operand {
                Some(place) => {
                    debug!("arg: {} {}", arg_place, place);
                    if !self.encoder.is_pure(called_def_id, Some(substs)) {
                        type_invs.push(
                            self.encoder
                                .encode_invariant_func_app(
                                    arg_ty,
                                    vir::Expr::snap_app(place.clone()),
                                )
                                .with_span(call_site_span)?,
                        );
                    }
                    fake_exprs.insert(arg_place, place);
                }
                None => {
                    // TODO(inv): also add invariant for constants?

                    // We have a constant.
                    constant_args.push(arg_place.clone());
                    let val_field = self
                        .encoder
                        .encode_value_field(arg_ty)
                        .with_span(call_site_span)?;

                    // TODO: String constants are not being encoded currently,
                    //       instead just inhale the permission to the value.
                    if !is_str(arg_ty) {
                        let arg_val_expr = self
                            .mir_encoder
                            .encode_operand_expr(mir_arg)
                            .with_span(call_site_span)?;
                        debug!("arg_val_expr: {} {}", arg_place, arg_val_expr);
                        fake_exprs.insert(arg_place.clone().field(val_field), arg_val_expr);
                    } else {
                        fake_expr_spans.insert(arg, call_site_span);
                        stmts.push(vir::Stmt::Inhale(vir::Inhale {
                            expr: vir::Expr::acc_permission(
                                arg_place.clone().field(val_field),
                                vir::PermAmount::Read,
                            ),
                        }));
                    }
                    let in_loop = self.loop_encoder.get_loop_depth(location.block) > 0;
                    if in_loop {
                        const_arg_vars.insert(arg_place);
                        return Err(SpannedEncodingError::unsupported(
                            format!(
                                "please use a local variable as argument for function '{full_func_proc_name}', not a \
                                constant, when calling the function from a loop"
                            ),
                            call_site_span,
                        ));
                    }
                }
            }
        }

        let (target_local, encoded_target) = {
            if target.is_some() {
                let (encoded_target, pre_stmts, ty, _) =
                    self.encode_place(destination, ArrayAccessKind::Shared, location)?;
                stmts.extend(pre_stmts);

                let target_local = if let Some(target_local) = destination.as_local() {
                    target_local.into()
                } else {
                    self.locals.get_fresh(ty)
                };
                fake_exprs.insert(
                    vir::Expr::local(self.encode_prusti_local(target_local)),
                    encoded_target.clone(),
                );
                (target_local, Some(encoded_target))
            } else {
                // The return type is Never
                // This means that the function call never returns
                // So, we `assume false` after the function call
                stmts_after.push(vir::Stmt::Inhale(vir::Inhale { expr: false.into() }));
                // Return a dummy local variable
                let never_ty = self.encoder.env().tcx().mk_ty_from_kind(ty::TyKind::Never);
                (self.locals.get_fresh(never_ty), None)
            }
        };

        let replace_fake_exprs = |mut expr: vir::Expr| -> vir::Expr {
            for (fake_arg, arg_expr) in fake_exprs.iter() {
                expr = expr
                    .fold_expr(|orig_expr| {
                        // Inline or skip usages of constant parameters
                        // See issue #85
                        match orig_expr {
                            // TODO(inv): what does this even do
                            /*
                            vir::Expr::FuncApp( vir::FuncApp {function_name: ref name, arguments: ref args, ..} ) => {
                                if args.len() == 1
                                    && args[0].is_local()
                                    && const_arg_vars.contains(&args[0])
                                {
                                    // Inline type invariant
                                    type_invs[name].inline_body(args.clone())
                                } else {
                                    orig_expr
                                }
                            }
                            */
                            vir::Expr::PredicateAccessPredicate(
                                vir::PredicateAccessPredicate { ref argument, .. },
                            ) => {
                                if argument.is_local() && const_arg_vars.contains(argument) {
                                    // Skip predicate permission
                                    true.into()
                                } else {
                                    orig_expr
                                }
                            }

                            x => x,
                        }
                    })
                    .replace_place(fake_arg, arg_expr);
            }
            expr
        };

        let procedure_contract = {
            self.encoder
                .get_procedure_contract_for_call(
                    self.proc_def_id,
                    called_def_id,
                    &arguments,
                    target_local,
                    substs,
                )
                .with_span(call_site_span)?
        };
        assert_one_magic_wand(procedure_contract.borrow_infos.len()).with_span(call_site_span)?;

        // Store a label for the pre state
        let pre_label = self.cfg_method.get_fresh_label_name();
        stmts.push(vir::Stmt::label(pre_label.clone()));

        // Havoc and inhale variables that store constants
        for constant_arg in &constant_args {
            stmts.extend(
                self.encode_havoc_and_initialization(constant_arg)
                    .with_span(call_site_span)?,
            );
        }

        // Encode precondition.
        let (pre_type_spec, pre_mandatory_type_spec, pre_invs_spec, pre_func_spec) =
            self.encode_precondition_expr(&procedure_contract, substs, fake_expr_spans)?;
        let pos = self.register_error(call_site_span, ErrorCtxt::ExhaleMethodPrecondition);
        stmts.push(vir::Stmt::Assert(vir::Assert {
            expr: replace_fake_exprs(pre_func_spec),
            position: pos,
        }));
        stmts.push(vir::Stmt::Assert(vir::Assert {
            expr: replace_fake_exprs(pre_invs_spec),
            position: pos,
        }));
        let pre_perm_spec = replace_fake_exprs(pre_type_spec);
        assert!(!pos.is_default());
        stmts.push(vir::Stmt::Exhale(vir::Exhale {
            expr: pre_perm_spec.remove_read_permissions(),
            position: pos,
        }));

        // Move all read permissions that are taken by magic wands into pre
        // state and exhale only before the magic wands are inhaled. In this
        // way we can have specifications that link shared reference arguments
        // and shared reference result.
        let pre_mandatory_perms: Vec<_> = pre_mandatory_type_spec
            .into_iter()
            .map(&replace_fake_exprs)
            .collect();
        let mut pre_mandatory_perms_old = Vec::new();
        for perm in pre_mandatory_perms {
            let from_place = perm.get_place().unwrap().clone();
            let to_place = from_place.clone().old(pre_label.clone());
            let old_perm = perm.replace_place(&from_place, &to_place);
            stmts.push(vir::Stmt::TransferPerm(vir::TransferPerm {
                left: from_place,
                right: to_place,
                unchecked: true,
            }));
            pre_mandatory_perms_old.push(old_perm);
        }
        let pre_mandatory_perm_spec = pre_mandatory_perms_old.into_iter().conjoin();

        // Havoc the content of the lhs, if there is one
        if let Some(ref target_place) = encoded_target {
            stmts.extend(self.encode_havoc(target_place).with_span(call_site_span)?);
        }

        // Store a label for permissions got back from the call
        debug!(
            "Procedure call location {:?} has label {}",
            location, pre_label
        );
        self.label_after_location
            .insert(location, pre_label.clone());

        // Store a label for the post state
        let post_label = self.cfg_method.get_fresh_label_name();

        let loan = self.polonius_info().get_call_loan_at_location(location);
        let (
            post_type_spec,
            return_type_spec,
            post_invs_spec,
            post_func_spec,
            magic_wands,
            read_transfer,
        ) = self.encode_postcondition_expr(
            Some(location),
            &procedure_contract,
            &pre_label,
            &post_label,
            Some((location, &fake_exprs)),
            encoded_target.is_none(),
            loan,
            false,
            substs,
        )?;
        // We inhale the magic wand just before applying it because we need
        // a magic wand that depends on the current value of ghost variables.
        let _magic_wands: Vec<_> = magic_wands
            .into_iter()
            .map(|magic_wand| {
                self.replace_old_places_with_ghost_vars(Some(&post_label), magic_wand)
            })
            .collect();

        let post_perm_spec = replace_fake_exprs(post_type_spec);
        stmts.push(vir::Stmt::Inhale(vir::Inhale {
            expr: post_perm_spec.remove_read_permissions(),
        }));
        if let Some(access) = return_type_spec {
            stmts.push(vir::Stmt::Inhale(vir::Inhale {
                expr: replace_fake_exprs(access),
            }));
        }
        for (from_place, to_place) in read_transfer {
            stmts.push(vir::Stmt::TransferPerm(vir::TransferPerm {
                left: replace_fake_exprs(from_place),
                right: replace_fake_exprs(to_place),
                unchecked: true,
            }));
        }
        stmts.push(vir::Stmt::Inhale(vir::Inhale {
            expr: replace_fake_exprs(post_invs_spec),
        }));
        stmts.push(vir::Stmt::Inhale(vir::Inhale {
            expr: replace_fake_exprs(post_func_spec),
        }));

        // Exhale the permissions that were moved into magic wands.
        assert!(!pos.is_default());
        stmts.push(vir::Stmt::Exhale(vir::Exhale {
            expr: pre_mandatory_perm_spec,
            position: pos,
        }));

        // Emit the label and magic wands
        stmts.push(vir::Stmt::label(post_label.clone()));

        stmts.extend(stmts_after);

        self.procedure_contracts
            .insert(location, (procedure_contract, fake_exprs));

        Ok(stmts)
    }

    #[allow(clippy::too_many_arguments)]
    #[tracing::instrument(level = "debug", skip(self))]
    fn encode_pure_function_call(
        &mut self,
        location: mir::Location,
        call_site_span: prusti_rustc_interface::span::Span,
        args: &[mir::Operand<'tcx>],
        destination: mir::Place<'tcx>,
        target: Option<BasicBlockIndex>,
        called_def_id: ProcedureDefId,
        call_substs: GenericArgsRef<'tcx>,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        let (function_name, return_type) = self
            .encoder
            .encode_pure_function_use(called_def_id, self.proc_def_id, call_substs)
            .with_span(call_site_span)?;
        debug!("Encoding pure function call '{}'", function_name);
        assert!(target.is_some());

        let mut arg_exprs = vec![];
        for operand in args.iter() {
            let arg_expr = self
                .mir_encoder
                .encode_operand_expr(operand)
                .with_span(call_site_span)?;
            arg_exprs.push(arg_expr);
        }

        self.encode_specified_pure_function_call(
            location,
            call_site_span,
            args,
            destination,
            target,
            function_name,
            arg_exprs,
            return_type,
            called_def_id,
            call_substs,
        )
    }

    #[allow(clippy::too_many_arguments)]
    fn encode_specified_pure_function_call(
        &mut self,
        location: mir::Location,
        call_site_span: Span,
        args: &[mir::Operand<'tcx>],
        destination: mir::Place<'tcx>,
        target: Option<BasicBlockIndex>,
        function_name: String,
        arg_exprs: Vec<vir::Expr>,
        return_type: Type,
        called_def_id: ProcedureDefId,
        call_substs: GenericArgsRef<'tcx>,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        let formal_args: Vec<vir::LocalVar> = args
            .iter()
            .enumerate()
            .map(|(i, arg)| {
                self.mir_encoder
                    .encode_operand_expr_type(arg)
                    .map(|ty| vir::LocalVar::new(format!("x{i}"), ty))
            })
            .collect::<Result<_, _>>()
            .with_span(call_site_span)?;

        let pos = self.register_error(call_site_span, ErrorCtxt::PureFunctionCall);

        let type_arguments = self
            .encoder
            .encode_generic_arguments(called_def_id, call_substs)
            .with_span(call_site_span)?;

        let func_call = vir::Expr::func_app(
            function_name,
            type_arguments,
            arg_exprs,
            formal_args,
            return_type.clone(),
            pos,
        );

        let (target_value, mut stmts) = self
            .encode_pure_function_call_lhs_value(destination, target, location)
            .with_span(call_site_span)?;

        let inhaled_expr = if return_type.is_domain() || return_type.is_snapshot() {
            let (target_place, pre_stmts) =
                self.encode_pure_function_call_lhs_place(destination, target, location)?;
            stmts.extend(pre_stmts);
            vir::Expr::eq_cmp(vir::Expr::snap_app(target_place), func_call)
        } else {
            vir::Expr::eq_cmp(target_value, func_call)
        };

        let (call_stmts, label) =
            self.encode_pure_function_call_site(location, destination, target, inhaled_expr)?;
        stmts.extend(call_stmts);

        self.encode_transfer_args_permissions(location, args, &mut stmts, &label, false)?;
        Ok(stmts)
    }

    fn encode_pure_function_call_lhs_value(
        &mut self,
        destination: mir::Place<'tcx>,
        target: Option<BasicBlockIndex>,
        location: mir::Location,
    ) -> SpannedEncodingResult<(vir::Expr, Vec<vir::Stmt>)> {
        let span = self.mir_encoder.get_span_of_location(location);
        assert!(target.is_some());
        let (encoded_place, pre_stmts, ty, _) =
            self.encode_place(destination, ArrayAccessKind::Shared, location)?;
        let encoded_lhs_value = self
            .encoder
            .encode_value_expr(encoded_place, ty)
            .with_span(span)?;
        Ok((encoded_lhs_value, pre_stmts))
    }

    fn encode_pure_function_call_lhs_place(
        &mut self,
        destination: mir::Place<'tcx>,
        target: Option<BasicBlockIndex>,
        location: mir::Location,
    ) -> SpannedEncodingResult<(vir::Expr, Vec<vir::Stmt>)> {
        assert!(target.is_some());
        let (encoded, pre_stmts, _, _) =
            self.encode_place(destination, ArrayAccessKind::Shared, location)?;
        Ok((encoded, pre_stmts))
    }

    #[tracing::instrument(level = "debug", skip(self))]
    fn encode_pure_function_call_site(
        &mut self,
        location: mir::Location,
        destination: mir::Place<'tcx>,
        target: Option<BasicBlockIndex>,
        call_result: vir::Expr,
    ) -> SpannedEncodingResult<(Vec<vir::Stmt>, String)> {
        let mut stmts = vec![];
        let span = self.mir_encoder.get_span_of_location(location);

        let label = self.cfg_method.get_fresh_label_name();
        stmts.push(vir::Stmt::label(label.clone()));

        // Havoc the content of the lhs
        let (target_place, pre_stmts) =
            self.encode_pure_function_call_lhs_place(destination, target, location)?;
        stmts.extend(pre_stmts);
        stmts.extend(self.encode_havoc(&target_place).with_span(span)?);
        let type_predicate = self
            .mir_encoder
            .encode_place_predicate_permission(target_place.clone(), vir::PermAmount::Write)
            .unwrap();

        stmts.push(vir::Stmt::Inhale(vir::Inhale {
            expr: type_predicate,
        }));

        // Initialize the lhs
        stmts.push(vir::Stmt::Inhale(vir::Inhale { expr: call_result }));

        // Store a label for permissions got back from the call
        debug!(
            "Pure function call location {:?} has label {}",
            location, label
        );
        self.label_after_location.insert(location, label.clone());

        Ok((stmts, label))
    }

    // Transfer the permissions for the arguments used in the call
    fn encode_transfer_args_permissions(
        &mut self,
        location: mir::Location,
        args: &[mir::Operand<'tcx>],
        stmts: &mut Vec<vir::Stmt>,
        label: &str,
        is_in_package_stmt: bool,
    ) -> SpannedEncodingResult<()> {
        let span = self.mir_encoder.get_span_of_location(location);
        for operand in args.iter() {
            let operand_ty = self.mir_encoder.get_operand_ty(operand);
            let operand_place = self
                .mir_encoder
                .encode_operand_place(operand)
                .with_span(span)?;
            match (operand_place, &operand_ty.kind()) {
                (Some(ref place), ty::TyKind::RawPtr(ty::TypeAndMut { ty: inner_ty, .. }))
                | (Some(ref place), ty::TyKind::Ref(_, inner_ty, _)) => {
                    let ref_field = self
                        .encoder
                        .encode_dereference_field(*inner_ty)
                        .with_span(span)?;
                    let ref_place = place.clone().field(ref_field);
                    stmts.extend(self.encode_transfer_permissions(
                        ref_place.clone(),
                        ref_place.clone().old(label),
                        location,
                        is_in_package_stmt,
                    ));
                }
                _ => {} // Nothing
            }
        }

        /*
        // Hack to work around the missing loan for arguments moved to the function call
        for operand in args.iter() {
            if let Some(place) = self.mir_encoder.encode_operand_place(operand) {
                debug!("Put permission {:?} in postcondition", place);
                // Choose the label that corresponds to the creation of the loan
                let (loans, _) = self.polonius_info().get_all_active_loans(location);
                let source_loans: Vec<_> = loans.iter().filter(|loan| {
                    let loan_places = self.polonius_info().get_loan_places(loan).unwrap();
                    let (expiring, _, restored) = self.encode_loan_places(&loan_places);
                    trace!("Try {:?} == {:?} | {:?}", expiring, place, restored);
                    expiring.parent() == Some(&place)
                }).collect();
                if !source_loans.is_empty() {
                    assert_eq!(source_loans.len(), 1, "The argument depends on a condition");
                    let source_loan = &source_loans[0];
                    let loan_loc = self.polonius_info().get_loan_location(&source_loan);
                    let loan_label = &self.label_after_location[&loan_loc];
                    stmts.push(vir::Stmt::TransferPerm(
                        place.clone(),
                        place.clone().old(&loan_label)
                    ));
                }
            }
        }
        */
        Ok(())
    }

    /// Encode permissions that are implicitly carried by the given local variable.
    /// `override_span` is used for local vars for fake expressions
    fn encode_local_variable_permission(
        &self,
        local: Local,
        override_span: Option<Span>,
    ) -> SpannedEncodingResult<vir::Expr> {
        Ok(match self.locals.get_type(local).kind() {
            ty::TyKind::Ref(_, ty, mutability) => {
                // Use unfolded references.
                let encoded_local = self.encode_prusti_local(local);
                let span = if let Some(fake_local_span) = override_span {
                    fake_local_span
                } else {
                    if self.mir.local_decls.get(local.into()).is_none() {
                        return Err(SpannedEncodingError::internal(
                            format!(
                                "In ProcedureEncoder::encode_local_variable_permission the local \
                                {local:?} is fake but override_span is None",
                            ),
                            self.mir.span,
                        ));
                    }
                    self.mir_encoder.get_local_span(local.into())
                };
                let field = self.encoder.encode_dereference_field(*ty).with_span(span)?;
                let place = vir::Expr::from(encoded_local).field(field);
                let perm_amount = match mutability {
                    Mutability::Mut => vir::PermAmount::Write,
                    Mutability::Not => vir::PermAmount::Read,
                };
                vir::Expr::and(
                    vir::Expr::acc_permission(place.clone(), vir::PermAmount::Write),
                    vir::Expr::pred_permission(place, perm_amount).unwrap(),
                )
            }
            _ => self
                .mir_encoder
                .encode_place_predicate_permission(
                    self.encode_prusti_local(local).into(),
                    vir::PermAmount::Write,
                )
                .unwrap(),
        })
    }

    /// Encode the precondition with three expressions:
    /// - one for the type encoding
    /// - one for the type invariants
    /// - one for the functional specification.
    #[allow(clippy::type_complexity)]
    #[tracing::instrument(level = "debug", skip(self, override_spans))]
    fn encode_precondition_expr(
        &self,
        contract: &ProcedureContract<'tcx>,
        substs: GenericArgsRef<'tcx>,
        override_spans: FxHashMap<Local, Span>, // spans for fake locals
    ) -> SpannedEncodingResult<(vir::Expr, Vec<vir::Expr>, vir::Expr, vir::Expr)> {
        let borrow_infos = &contract.borrow_infos;
        let maybe_blocked_paths = if !borrow_infos.is_empty() {
            assert_eq!(
                borrow_infos.len(),
                1,
                "We can have at most one magic wand in the postcondition."
            );
            let borrow_info = &borrow_infos[0];
            Some(&borrow_info.blocked_paths)
        } else {
            None
        };
        // Type spec in which read permissions can be removed.
        let mut type_spec = Vec::new();
        // Type spec containing the read permissions that must be exhaled because they were
        // moved into a magic wand.
        let mut mandatory_type_spec = Vec::new();
        fn is_blocked(maybe_blocked_paths: Option<&Vec<(Place, Mutability)>>, arg: Local) -> bool {
            if let Some(blocked_paths) = maybe_blocked_paths {
                for (blocked_place, _) in blocked_paths {
                    if blocked_place.is_root(arg) {
                        return true;
                    }
                }
            }
            false
        }
        for local in &contract.args {
            let mut add = |access: vir::Expr| {
                if is_blocked(maybe_blocked_paths, *local)
                    && access.get_perm_amount() == vir::PermAmount::Read
                {
                    mandatory_type_spec.push(access);
                } else {
                    type_spec.push(access);
                }
            };
            let access =
                self.encode_local_variable_permission(*local, override_spans.get(local).copied())?;
            match access {
                vir::Expr::BinOp(vir::BinOp {
                    op_kind: vir::BinaryOpKind::And,
                    left: box access1,
                    right: box access2,
                    ..
                }) => {
                    add(access1);
                    add(access2);
                }
                _ => add(access),
            };
        }

        // Encode functional specification
        let encoded_args: Vec<vir::Expr> = contract
            .args
            .iter()
            .map(|local| self.encode_prusti_local(*local).into())
            .collect();

        let func_spec: Vec<vir::Expr> = contract
            .functional_precondition(self.encoder.env(), substs)
            .iter()
            .map(|(assertion, assertion_substs)| {
                self.encoder.encode_assertion(
                    assertion,
                    None,
                    &encoded_args,
                    None,
                    false,
                    self.proc_def_id,
                    assertion_substs,
                )
            })
            .collect::<Result<Vec<_>, _>>()?;

        // TODO(tymap): do this with the previous step ...
        let precondition_spans = MultiSpan::from_spans(
            contract
                .functional_precondition(self.encoder.env(), substs)
                .iter()
                .map(|(ts, _)| self.encoder.env().query.get_def_span(ts))
                .collect(),
        );

        let mut invs_spec: Vec<vir::Expr> = vec![];
        for arg in contract.args.iter() {
            // FIXME: this is somewhat hacky to avoid consistency errors with raw_ref args. this
            // assumes that invariants for raw_ref types are always empty.
            let ty = self.locals.get_type(*arg);
            if !ty.is_unsafe_ptr() && !self.encoder.is_pure(contract.def_id, Some(substs)) {
                invs_spec.push(
                    self.encoder
                        .encode_invariant_func_app(ty, self.encode_prusti_local(*arg).into())
                        .with_span(precondition_spans.clone())?,
                );
            }
        }
        Ok((
            type_spec.into_iter().conjoin(),
            mandatory_type_spec,
            invs_spec.into_iter().conjoin(),
            func_spec.into_iter().conjoin(),
        ))
    }

    #[tracing::instrument(level = "debug", skip(self))]
    fn encode_spec_refinement(
        &self,
        pre_label: &str,
    ) -> SpannedEncodingResult<(
        Option<PreconditionWeakening>,
        Option<PostconditionStrengthening>,
    )> {
        // Encode arguments and return
        let encoded_args = self
            .procedure_contract()
            .args
            .iter()
            .map(|local| self.encode_prusti_local(*local).into())
            .collect::<Vec<_>>();
        let encoded_return = self
            .encode_prusti_local(self.procedure_contract().returned_value)
            .into();

        debug!("procedure_contract: {:?}", self.procedure_contract());

        let procedure_spec = &self.procedure_contract().specification;

        let mut weakening: Option<PreconditionWeakening> = None;
        let mut strengthening: Option<PostconditionStrengthening> = None;

        if let SpecificationItem::Refined(from, to) = &procedure_spec.pres {
            // See comment in `ProcedureContractGeneric::functional_precondition`.
            let trait_substs = self
                .encoder
                .env()
                .query
                .find_trait_method_substs(self.proc_def_id, self.substs)
                .unwrap()
                .1;

            let from_pre = from
                .iter()
                .map(|spec| {
                    self.encoder.encode_assertion(
                        spec,
                        None,
                        &encoded_args,
                        None,
                        false,
                        self.proc_def_id,
                        trait_substs,
                    )
                })
                .collect::<Result<Vec<_>, _>>()?
                .into_iter()
                .conjoin();
            let to_pre = to
                .iter()
                .map(|spec| {
                    self.encoder.encode_assertion(
                        spec,
                        None,
                        &encoded_args,
                        None,
                        false,
                        self.proc_def_id,
                        self.substs,
                    )
                })
                .collect::<Result<Vec<_>, _>>()?
                .into_iter()
                .conjoin();

            // The spans are used for error reporting
            let spec_functions_span = MultiSpan::from_spans(
                from.iter()
                    .chain(to.iter())
                    .map(|spec_def_id| self.encoder.env().query.get_def_span(spec_def_id))
                    .collect(),
            );

            weakening = Some(RefinementCheckExpr {
                spec_functions_span,
                refinement_check_expr: vir_expr! {[from_pre] ==> [to_pre]},
            });
        }

        if let SpecificationItem::Refined(from, to) = &procedure_spec.posts {
            // See comment in `ProcedureContractGeneric::functional_precondition`.
            let trait_substs = self
                .encoder
                .env()
                .query
                .find_trait_method_substs(self.proc_def_id, self.substs)
                .unwrap()
                .1;

            let from_post = from
                .iter()
                .map(|spec| {
                    self.encoder.encode_assertion(
                        spec,
                        Some(pre_label),
                        &encoded_args,
                        Some(&encoded_return),
                        false,
                        self.proc_def_id,
                        trait_substs,
                    )
                })
                .collect::<Result<Vec<_>, _>>()?
                .into_iter()
                .conjoin();
            let to_post = to
                .iter()
                .map(|spec| {
                    self.encoder.encode_assertion(
                        spec,
                        Some(pre_label),
                        &encoded_args,
                        Some(&encoded_return),
                        false,
                        self.proc_def_id,
                        self.substs,
                    )
                })
                .collect::<Result<Vec<_>, _>>()?
                .into_iter()
                .conjoin();

            // The spans are used for error reporting
            let spec_functions_span = MultiSpan::from_spans(
                from.iter()
                    .chain(to.iter())
                    .map(|spec_def_id| self.encoder.env().query.get_def_span(spec_def_id))
                    .collect(),
            );

            let strengthening_expr = self.wrap_arguments_into_old(
                vir_expr! {
                    [to_post] ==> [from_post]
                },
                pre_label,
                self.procedure_contract(),
                &encoded_args,
            )?;

            strengthening = Some(PostconditionStrengthening {
                spec_functions_span,
                refinement_check_expr: strengthening_expr,
            });
        }

        if let SpecificationItem::Refined(from, to) = &procedure_spec.pledges {
            if !from.is_empty() || to.iter().any(|p| p.lhs.is_some()) {
                unimplemented!("Refining specifications with pledges is not supported");
            }
            // If the trait has no pledges and the implementer only makes additional guarantees
            // then the refinement is safe
        }

        Ok((weakening, strengthening))
    }

    /// Encode precondition inhale on the definition side.
    #[tracing::instrument(level = "debug", skip_all)]
    fn encode_preconditions(
        &mut self,
        start_cfg_block: CfgBlockIndex,
        weakening_spec: Option<PreconditionWeakening>,
    ) -> SpannedEncodingResult<()> {
        self.cfg_method
            .add_stmt(start_cfg_block, vir::Stmt::comment("Preconditions:"));
        let (type_spec, mandatory_type_spec, invs_spec, func_spec) = self
            .encode_precondition_expr(
                self.procedure_contract(),
                self.substs,
                FxHashMap::default(),
            )?;
        self.cfg_method.add_stmt(
            start_cfg_block,
            vir::Stmt::Inhale(vir::Inhale { expr: type_spec }),
        );
        self.cfg_method.add_stmt(
            start_cfg_block,
            vir::Stmt::Inhale(vir::Inhale {
                expr: mandatory_type_spec.into_iter().conjoin(),
            }),
        );
        self.cfg_method.add_stmt(
            start_cfg_block,
            vir::Stmt::Inhale(vir::Inhale { expr: invs_spec }),
        );
        // Weakening assertion must be put before inhaling the precondition, otherwise the weakening
        // soundness check becomes trivially satisfied.
        if let Some(weakening_spec) = weakening_spec {
            let pos = self.register_error(
                weakening_spec.spec_functions_span,
                ErrorCtxt::AssertMethodPreconditionWeakening,
            );
            self.cfg_method.add_stmt(
                start_cfg_block,
                vir::Stmt::Assert(vir::Assert {
                    expr: weakening_spec.refinement_check_expr,
                    position: pos,
                }),
            );
        }
        self.cfg_method.add_stmt(
            start_cfg_block,
            vir::Stmt::Inhale(vir::Inhale { expr: func_spec }),
        );
        self.cfg_method
            .add_stmt(start_cfg_block, vir::Stmt::label(PRECONDITION_LABEL));
        Ok(())
    }

    /// Encode the magic wand used in the postcondition with its
    /// functional specification. Returns (lhs, rhs).
    #[tracing::instrument(level = "debug", skip(self))]
    fn encode_postcondition_magic_wand(
        &self,
        location: Option<mir::Location>,
        contract: &ProcedureContract<'tcx>,
        pre_label: &str,
        post_label: &str,
        substs: GenericArgsRef<'tcx>,
    ) -> EncodingResult<Option<(vir::Expr, vir::Expr)>> {
        let span = if let Some(loc) = location {
            self.mir.source_info(loc).span
        } else {
            self.mir.span
        };

        // Encode args and return.
        let encoded_args: Vec<vir::Expr> = contract
            .args
            .iter()
            .map(|local| self.encode_prusti_local(*local).into())
            .collect();
        let encoded_return: vir::Expr = self.encode_prusti_local(contract.returned_value).into();

        // Encode magic wands
        let borrow_infos = &contract.borrow_infos;
        if !borrow_infos.is_empty() {
            assert_eq!(
                borrow_infos.len(),
                1,
                "We can have at most one magic wand in the postcondition."
            );
            let borrow_info = &borrow_infos[0];
            let pledges: Vec<&Pledge> = contract.pledges().collect();
            assert!(
                pledges.len() <= 1,
                "There can be at most one pledge in the function postcondition."
            );
            debug!("borrow_info {:?}", borrow_info);
            let encode_place_perm = |place, mutability, label| -> _ {
                let perm_amount = match mutability {
                    Mutability::Not => vir::PermAmount::Read,
                    Mutability::Mut => vir::PermAmount::Write,
                };
                let (place_expr, place_ty, _) = self
                    .encode_generic_place(contract.def_id, location, place)
                    .with_span(span)?;
                let vir_access =
                    vir::Expr::pred_permission(place_expr.clone().old(label), perm_amount).unwrap();
                if !self.encoder.is_pure(contract.def_id, Some(substs)) {
                    let inv = self
                        .encoder
                        .encode_invariant_func_app(place_ty, place_expr.old(label))
                        .with_span(span)?;
                    Ok(vir::Expr::and(vir_access, inv))
                } else {
                    Ok(vir_access)
                }
            };
            let mut lhs: Vec<_> = borrow_info
                .blocking_paths
                .iter()
                .map(|(place, mutability)| encode_place_perm(*place, *mutability, post_label))
                .collect::<SpannedEncodingResult<_>>()?;
            let mut rhs: Vec<_> = borrow_info
                .blocked_paths
                .iter()
                .map(|(place, mutability)| encode_place_perm(*place, *mutability, pre_label))
                .collect::<SpannedEncodingResult<_>>()?;
            if let Some(typed::Pledge {
                reference,
                lhs: body_lhs,
                rhs: body_rhs,
            }) = pledges.first()
            {
                debug!(
                    "pledge reference={:?} lhs={:?} rhs={:?}",
                    reference, body_lhs, body_rhs
                );
                assert!(
                    reference.is_none(),
                    "The reference should be none in postcondition."
                );
                let mut assertion_lhs = if let Some(body_lhs) = body_lhs {
                    self.encoder.encode_assertion(
                        body_lhs,
                        Some(pre_label),
                        &encoded_args,
                        Some(&encoded_return),
                        false,
                        self.proc_def_id,
                        substs,
                    )?
                } else {
                    true.into()
                };
                let mut assertion_rhs = self.encoder.encode_assertion(
                    body_rhs,
                    Some(pre_label),
                    &encoded_args,
                    Some(&encoded_return),
                    false,
                    self.proc_def_id,
                    substs,
                )?;
                assertion_lhs = self.wrap_arguments_into_old(
                    assertion_lhs,
                    pre_label,
                    contract,
                    &encoded_args,
                )?;
                assertion_rhs = self.wrap_arguments_into_old(
                    assertion_rhs,
                    pre_label,
                    contract,
                    &encoded_args,
                )?;
                let ty = self.locals.get_type(contract.returned_value);
                let return_span = self
                    .mir_encoder
                    .get_local_span(contract.returned_value.into());
                let (encoded_deref, ..) = self
                    .mir_encoder
                    .encode_deref(encoded_return, ty)
                    .with_span(return_span)?;

                let original_expr = encoded_deref;
                let old_expr = vir::Expr::labelled_old(post_label, original_expr.clone());
                // TODO ??
                assertion_lhs = assertion_lhs.replace_place(&original_expr, &old_expr);
                assertion_lhs = assertion_lhs.remove_redundant_old();
                assertion_rhs = assertion_rhs.replace_place(&original_expr, &old_expr);
                assertion_rhs = assertion_rhs.remove_redundant_old();
                lhs.push(assertion_lhs);
                rhs.push(assertion_rhs);
            }
            let lhs = lhs.into_iter().conjoin();
            let rhs = rhs.into_iter().conjoin();
            Ok(Some((lhs, rhs)))
        } else {
            Ok(None)
        }
    }

    /// Wrap function arguments used in the postcondition into ``old``:
    ///
    /// +   For references wrap the base ``_1.var_ref``.
    /// +   For non-references wrap the entire place into old.
    fn wrap_arguments_into_old(
        &self,
        mut assertion: vir::Expr,
        pre_label: &str,
        contract: &ProcedureContract<'tcx>,
        encoded_args: &[vir::Expr],
    ) -> SpannedEncodingResult<vir::Expr> {
        for (encoded_arg, &arg) in encoded_args.iter().zip(&contract.args) {
            let ty = self.locals.get_type(arg);
            if is_reference(ty) {
                // If the argument is a reference, we wrap _1.val_ref into old.
                let arg_span = self.mir_encoder.get_local_span(arg.into());
                let (encoded_deref, ..) = self
                    .mir_encoder
                    .encode_deref(encoded_arg.clone(), ty)
                    .with_span(arg_span)?;
                let original_expr = encoded_deref;
                let old_expr = original_expr.clone().old(pre_label);
                assertion = assertion.replace_place(&original_expr, &old_expr);
            } else {
                // If the argument is not a reference, we wrap entire path into old.
                assertion = assertion.fold_expr(|e| {
                    if let vir::Expr::FuncApp(vir::FuncApp {
                        function_name,
                        arguments,
                        ..
                    }) = &e
                    {
                        // If `assertion` is e.g. a `foo(snap(_1))` with an `_1: T` and `fn foo(x: &T)` we cannot
                        // wrap `foo(snap(old[pre](_1)))`, but should instead wrap as `foo(old[pre](snap(_1)))`
                        // TODO: this could all be fixed by making all arguments into fields (e.g. `_1.local`).
                        // This would also make mutating of arguments sound.
                        if function_name == "snap$" && &arguments[0] == encoded_arg {
                            return e.old(pre_label);
                        }
                    } else if e.is_place() {
                        // Check the base of the path matches the current arg:
                        let base: vir::Expr = e.get_base().into();
                        if encoded_arg == &base {
                            return e.old(pre_label);
                        }
                    }
                    e
                });
            }
        }
        Ok(assertion.remove_redundant_old())
    }

    /// Encode the postcondition with three expressions:
    /// - one for the type encoding
    /// - one for the type invariants
    /// - one for the functional specification.
    /// Also return the magic wands to be added to the postcondition.
    ///
    /// `function_end` – are we encoding the exhale of the postcondition
    /// at the end of the method?
    #[allow(clippy::too_many_arguments, clippy::type_complexity)]
    #[tracing::instrument(level = "debug", skip(self))]
    fn encode_postcondition_expr(
        &mut self,
        location: Option<mir::Location>,
        contract: &ProcedureContract<'tcx>,
        pre_label: &str,
        post_label: &str,
        magic_wand_store_info: Option<(mir::Location, &FxHashMap<vir::Expr, vir::Expr>)>,
        _diverging: bool,
        loan: Option<facts::Loan>,
        function_end: bool,
        substs: GenericArgsRef<'tcx>,
    ) -> SpannedEncodingResult<(
        vir::Expr,                   // Returned permissions from types.
        Option<vir::Expr>,           // Permission of the return value.
        vir::Expr,                   // Invariants.
        vir::Expr,                   // Functional specification.
        Vec<vir::Expr>,              // Magic wands.
        Vec<(vir::Expr, vir::Expr)>, // Read permissions that need to be transferred to a new place.
    )> {
        let mut type_spec = vec![];
        let mut invs_spec = vec![];
        let mut read_transfer = vec![]; // Permissions taken as read
                                        // references that need to
                                        // be transfered to old.

        // Encode the permissions got back and invariants for the arguments of type reference
        for (place, mutability) in contract.returned_refs.iter() {
            debug!(
                "Put permission {:?} ({:?}) in postcondition",
                place, mutability
            );
            // TODO: Use a better span
            let (place_expr, place_ty, _) = self
                .encode_generic_place(contract.def_id, location, *place)
                .with_span(self.mir.span)?;
            let old_place_expr = place_expr.clone().old(pre_label);
            let mut add_type_spec = |perm_amount| {
                let permissions =
                    vir::Expr::pred_permission(old_place_expr.clone(), perm_amount).unwrap();
                type_spec.push(permissions);
            };
            match mutability {
                Mutability::Not => {
                    if function_end {
                        add_type_spec(vir::PermAmount::Read);
                    }
                    read_transfer.push((place_expr, old_place_expr));
                }
                Mutability::Mut => {
                    add_type_spec(vir::PermAmount::Write);
                    if !self.encoder.is_pure(contract.def_id, Some(substs)) {
                        let inv = self
                            .encoder
                            .encode_invariant_func_app(place_ty, old_place_expr)
                            // TODO: Use a better span
                            .with_span(self.mir.span)?;
                        invs_spec.push(inv);
                    }
                }
            };
        }

        // Encode args and return.
        let encoded_args: Vec<vir::Expr> = contract
            .args
            .iter()
            .map(|local| self.encode_prusti_local(*local).into())
            .collect();
        trace!(
            "encode_postcondition_expr: encoded_args {:?} ({:?}) as {:?}",
            contract.args,
            contract
                .args
                .iter()
                .map(|a| self.locals.get_type(*a))
                .collect::<Vec<_>>(),
            encoded_args
        );

        let encoded_return: vir::Expr = self.encode_prusti_local(contract.returned_value).into();

        let span = if let Some(loc) = location {
            self.mir.source_info(loc).span
        } else {
            self.mir.span
        };
        let mut magic_wands = Vec::new();
        if let Some((mut lhs, mut rhs)) = self
            .encode_postcondition_magic_wand(location, contract, pre_label, post_label, substs)
            .with_span(span)?
        {
            if let Some((location, fake_exprs)) = magic_wand_store_info {
                let replace_fake_exprs = |mut expr: vir::Expr| -> vir::Expr {
                    for (fake_arg, arg_expr) in fake_exprs.iter() {
                        expr = expr.replace_place(fake_arg, arg_expr);
                    }
                    expr
                };
                lhs = replace_fake_exprs(lhs);
                rhs = replace_fake_exprs(rhs);
                lhs = self.encoder.patch_snapshots(lhs).with_span(self.mir.span)?;
                rhs = self.encoder.patch_snapshots(rhs).with_span(self.mir.span)?;
                debug!("Insert ({:?} {:?}) at {:?}", lhs, rhs, location);
                self.magic_wand_at_location
                    .insert(location, (post_label.to_string(), lhs.clone(), rhs.clone()));
            }
            magic_wands.push(vir::Expr::magic_wand(
                lhs,
                rhs,
                loan.map(|l| l.index().into()),
            ));
        }

        // Encode permissions for return type
        // TODO: Clean-up: remove unnecessary Option.
        let return_perm =
            Some(self.encode_local_variable_permission(contract.returned_value, None)?);

        // Encode functional specification
        let mut func_spec = vec![];
        let mut func_spec_spans = vec![];
        let func_postcondition = contract.functional_postcondition(self.encoder.env(), substs);
        for (typed_assertion, assertion_substs) in func_postcondition {
            let mut assertion = self.encoder.encode_assertion(
                &typed_assertion,
                Some(pre_label),
                &encoded_args,
                Some(&encoded_return),
                false,
                self.proc_def_id,
                assertion_substs,
            )?;
            let assertion_span = self.encoder.env().query.get_def_span(typed_assertion);
            func_spec_spans.push(assertion_span);
            let assertion_pos = self.mir_encoder.register_span(assertion_span);
            assertion =
                self.wrap_arguments_into_old(assertion, pre_label, contract, &encoded_args)?;
            func_spec.push(assertion.set_default_pos(assertion_pos));
        }
        let postcondition_span = MultiSpan::from_spans(func_spec_spans);
        let func_spec_pos = self.mir_encoder.register_span(postcondition_span.clone());

        // Encode invariant for return value
        if !self.encoder.is_pure(contract.def_id, Some(substs)) {
            invs_spec.push(
                self.encoder
                    .encode_invariant_func_app(
                        self.locals.get_type(contract.returned_value),
                        encoded_return,
                    )
                    .with_span(postcondition_span)?,
            );
        }

        let full_func_spec = func_spec
            .into_iter()
            .conjoin()
            .set_default_pos(func_spec_pos);

        Ok((
            type_spec.into_iter().conjoin(),
            return_perm,
            invs_spec.into_iter().conjoin(),
            full_func_spec,
            magic_wands,
            read_transfer,
        ))
    }

    /// Modelling move as simple assignment on Viper level has a consequence
    /// that the assigned place changes. Therefore, if some value is
    /// moved into a borrow, the borrow starts pointing to a different
    /// memory location. As a result, we cannot use old expressions as
    /// roots for holding permissions because they always point to the
    /// same place. Instead, we replace them with ghost variables.
    ///
    /// This method replaces all places with `label` with ghost variables.
    #[tracing::instrument(level = "trace", skip(self))]
    fn replace_old_places_with_ghost_vars(
        &mut self,
        label: Option<&str>,
        expr: vir::Expr,
    ) -> vir::Expr {
        struct OldReplacer<'a> {
            label: Option<&'a str>,
            old_to_ghost_var: &'a mut FxHashMap<vir::Expr, vir::Expr>,
            old_ghost_vars: &'a mut FxHashMap<String, vir::Type>,
            cfg_method: &'a mut vir::CfgMethod,
        }
        impl<'a> vir::ExprFolder for OldReplacer<'a> {
            #[allow(clippy::map_entry)]
            fn fold_labelled_old(
                &mut self,
                vir::LabelledOld {
                    label,
                    base,
                    position,
                }: vir::LabelledOld,
            ) -> vir::Expr {
                let base = self.fold_boxed(base);
                let expr = vir::Expr::LabelledOld(vir::LabelledOld {
                    label: label.clone(),
                    base,
                    position,
                });
                debug!(
                    "replace_old_places_with_ghost_vars({:?}, {})",
                    self.label, expr
                );
                if self.old_to_ghost_var.contains_key(&expr) {
                    debug!("found={}", self.old_to_ghost_var[&expr]);
                    self.old_to_ghost_var[&expr].clone().set_pos(position)
                } else if self.label == Some(&label) {
                    let mut counter = 0;
                    let mut name = format!("_old${label}${counter}");
                    while self.old_ghost_vars.contains_key(&name) {
                        counter += 1;
                        name = format!("_old${label}${counter}");
                    }
                    let vir_type = expr.get_type().clone();
                    self.old_ghost_vars.insert(name.clone(), vir_type.clone());
                    self.cfg_method.add_local_var(&name, vir_type.clone());
                    let var: vir::Expr = vir::LocalVar::new(name, vir_type).into();
                    self.old_to_ghost_var.insert(expr, var.clone());
                    var
                } else {
                    debug!("not found");
                    expr
                }
            }
        }
        let mut replacer = OldReplacer {
            label,
            old_to_ghost_var: &mut self.old_to_ghost_var,
            old_ghost_vars: &mut self.old_ghost_vars,
            cfg_method: &mut self.cfg_method,
        };
        vir::ExprFolder::fold(&mut replacer, expr)
    }

    /// Encode the package statement of magic wands at the end of the method
    #[tracing::instrument(level = "debug", skip(self))]
    fn encode_package_end_of_method(
        &mut self,
        pre_label: &str,
        post_label: &str,
        location: mir::Location,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        let mut stmts = Vec::new();
        let span = self.mir.source_info(location).span;

        // Package magic wand(s)
        if let Some((lhs, rhs)) = self
            .encode_postcondition_magic_wand(
                None,
                self.procedure_contract(),
                pre_label,
                post_label,
                self.substs,
            )
            .with_span(span)?
        {
            let pos =
                self.register_error(self.mir.span, ErrorCtxt::PackageMagicWandForPostcondition);

            let blocker = mir::RETURN_PLACE;
            // TODO: Check if it really is always start and not the mid point.
            let start_point = self
                .polonius_info()
                .get_point(location, facts::PointType::Start);

            let opt_region = self.polonius_info().place_regions.for_local(blocker);
            let mut package_stmts = if let Some(region) = opt_region {
                let (all_loans, zombie_loans) = self
                    .polonius_info()
                    .get_all_loans_kept_alive_by(start_point, region);
                self.encode_expiration_of_loans(all_loans, &zombie_loans, location, None, true)?
            } else {
                // This happens when encoding the following function
                // ```
                // struct MyStruct<'tcx>(TyCtxt<'tcx>);
                // fn foo(tcx: TyCtxt) -> MyStruct {
                //     MyStruct(tcx)
                // }
                // ```
                return Err(SpannedEncodingError::unsupported(
                    "the encoding of pledges does not supporte this \
                        kind of reborrowing",
                    self.mir_encoder.get_span_of_location(location),
                ));
            };

            // We need to make sure that the lhs of the magic wand is
            // fully folded before the label.
            // To do so, we need to use the lhs without functional specification.
            let current_lhs = lhs
                .clone()
                .map_labels(|label| {
                    if label == post_label {
                        None
                    } else {
                        Some(label)
                    }
                })
                .filter_perm_conjunction();
            stmts.extend(self.encode_obtain(current_lhs, pos));

            // lhs must be phrased in terms of post state.
            let post_label = post_label.to_string();
            stmts.push(vir::Stmt::label(post_label.clone()));

            // Make the deref of reference arguments to be folded (see issue #47)
            package_stmts.push(vir::Stmt::comment("Fold predicates for &mut args"));
            for arg_index in self.mir.args_iter() {
                let arg_ty = self.mir.local_decls[arg_index].ty;
                let arg_span = self.mir_encoder.get_local_span(arg_index);
                if is_reference(arg_ty) {
                    let encoded_arg = self.mir_encoder.encode_local(arg_index)?;
                    let (deref_place, ..) = self
                        .mir_encoder
                        .encode_deref(encoded_arg.into(), arg_ty)
                        .with_span(arg_span)?;
                    let old_deref_place = deref_place.clone().old(pre_label);
                    package_stmts.extend(self.encode_transfer_permissions(
                        deref_place,
                        old_deref_place.clone(),
                        location,
                        true,
                    ));
                    let predicate =
                        vir::Expr::pred_permission(old_deref_place, vir::PermAmount::Write)
                            .unwrap();
                    package_stmts.extend(self.encode_obtain(predicate, pos));
                }
            }

            // The fold-unfold algorithm will fill the body of the package statement
            let vars: Vec<_> = self
                .old_ghost_vars
                .iter()
                .map(|(name, typ)| vir::LocalVar::new(name.clone(), typ.clone()))
                .collect();
            stmts.push(vir::Stmt::package_magic_wand(
                lhs,
                rhs,
                package_stmts,
                post_label.clone(),
                vars,
                pos,
            ));

            // We need to transfer all permissions from old[post](lhs) to lhs.
            let borrow_infos = &self.procedure_contract().borrow_infos;
            assert_eq!(
                borrow_infos.len(),
                1,
                "We can have at most one magic wand in the postcondition."
            );
            for (path, _) in borrow_infos[0].blocking_paths.clone().iter() {
                let (encoded_place, _, _) = self
                    .encode_generic_place(self.procedure_contract().def_id, None, *path)
                    .with_span(span)?;
                let old_place = encoded_place.clone().old(post_label.clone());
                stmts.extend(self.encode_transfer_permissions(
                    old_place,
                    encoded_place,
                    location,
                    true,
                ));
            }
        }

        Ok(stmts)
    }

    /// Encode postcondition exhale in the `return_cfg_block` CFG block.
    #[tracing::instrument(level = "debug", skip_all)]
    fn encode_postconditions(
        &mut self,
        return_cfg_block: CfgBlockIndex,
        strengthening_spec: Option<PostconditionStrengthening>,
    ) -> SpannedEncodingResult<()> {
        // This clone is only due to borrow checker restrictions
        let contract = self.procedure_contract().clone();

        self.cfg_method
            .add_stmt(return_cfg_block, vir::Stmt::comment("Exhale postcondition"));

        let postcondition_label = self.cfg_method.get_fresh_label_name();
        self.cfg_method.add_stmt(
            return_cfg_block,
            vir::Stmt::label(postcondition_label.clone()),
        );

        let (type_spec, return_type_spec, invs_spec, func_spec, magic_wands, _) = self
            .encode_postcondition_expr(
                None,
                &contract,
                PRECONDITION_LABEL,
                &postcondition_label,
                None,
                false,
                None,
                true,
                self.substs,
            )?;

        let type_inv_pos = self.register_error(
            self.mir.span,
            ErrorCtxt::AssertMethodPostconditionTypeInvariants,
        );

        // Find which arguments are blocked by the returned reference.
        let blocked_args: Vec<usize> = {
            let borrow_infos = &contract.borrow_infos;
            if !borrow_infos.is_empty() {
                assert_eq!(
                    borrow_infos.len(),
                    1,
                    "We can have at most one magic wand in the postcondition."
                );
                let mut blocked_args = Vec::new();
                for (blocked_place, _) in &borrow_infos[0].blocked_paths {
                    for (i, arg) in contract.args.iter().enumerate() {
                        debug!("blocked_place={:?} i={:?} arg={:?}", blocked_place, i, arg);
                        if blocked_place.is_root(*arg) {
                            blocked_args.push(i);
                        }
                    }
                }
                blocked_args
            } else {
                Vec::new()
            }
        };

        // Transfer borrow permissions to old.
        self.cfg_method.add_stmt(
            return_cfg_block,
            vir::Stmt::comment(
                "Fold predicates for &mut args and transfer borrow permissions to old",
            ),
        );
        for (i, &arg) in contract.args.iter().enumerate() {
            if blocked_args.contains(&i) {
                // Permissions of arguments that are blocked by the returned reference are not
                // added to the postcondition.
                continue;
            }
            let ty = self.locals.get_type(arg);
            if is_reference(ty) {
                let encoded_arg: vir::Expr = self.encode_prusti_local(arg).into();
                let arg_span = self.mir_encoder.get_local_span(arg.into());
                let (encoded_deref, ..) = self
                    .mir_encoder
                    .encode_deref(encoded_arg.clone(), ty)
                    .with_span(arg_span)?;

                // Fold argument.
                let deref_pred = self
                    .mir_encoder
                    .encode_place_predicate_permission(
                        encoded_deref.clone(),
                        vir::PermAmount::Write,
                    )
                    .unwrap();
                for stmt in self.encode_obtain(deref_pred, type_inv_pos).drain(..) {
                    self.cfg_method.add_stmt(return_cfg_block, stmt);
                }

                // Transfer permissions.
                //
                // TODO: This version does not allow mutating function arguments.
                // A way to allow this would be for each reference typed
                // argument generate a fresh pure variable `v` and a
                // variable `b:=true` and add `old[pre](_1.val_ref)` to
                // the replacement map. Before each assignment that
                // assigns to the reference itself, emit `b:=false`.
                // After each assignment that assigns to the contents
                // the reference is pointing to emit:
                //
                //      if b {
                //          v := _1.val_ref;
                //      }
                let old_expr = encoded_deref.clone().old(PRECONDITION_LABEL);
                let name = format!("_old${PRECONDITION_LABEL}${i}");
                let vir_type = old_expr.get_type().clone();
                self.old_ghost_vars.insert(name.clone(), vir_type.clone());
                self.cfg_method.add_local_var(&name, vir_type.clone());
                let var: vir::Expr = vir::LocalVar::new(name, vir_type).into();
                self.old_to_ghost_var.insert(old_expr, var.clone());

                self.cfg_method.add_stmt(
                    return_cfg_block,
                    vir::Stmt::Assign(vir::Assign {
                        target: var,
                        source: encoded_deref,
                        kind: vir::AssignKind::Move,
                    }),
                );
            }
        }

        // Fold the result.
        self.cfg_method
            .add_stmt(return_cfg_block, vir::Stmt::comment("Fold the result"));
        let ty = self.locals.get_type(contract.returned_value);
        let encoded_return: vir::Expr = self.encode_prusti_local(contract.returned_value).into();
        let return_span = self
            .mir_encoder
            .get_local_span(contract.returned_value.into());
        let encoded_return_expr = if is_reference(ty) {
            let (encoded_deref, ..) = self
                .mir_encoder
                .encode_deref(encoded_return, ty)
                .with_span(return_span)?;
            encoded_deref
        } else {
            encoded_return
        };
        let return_pred = self
            .mir_encoder
            .encode_place_predicate_permission(encoded_return_expr, vir::PermAmount::Write)
            .unwrap();
        let obtain_return_stmt = vir::Stmt::Obtain(vir::Obtain {
            expr: return_pred,
            position: type_inv_pos,
        });
        self.cfg_method
            .add_stmt(return_cfg_block, obtain_return_stmt);

        // Assert possible strengthening
        self.cfg_method.add_stmt(
            return_cfg_block,
            vir::Stmt::comment("Assert possible strengthening"),
        );
        if let Some(strengthening_spec) = strengthening_spec {
            let patched_strengthening_spec = self
                .replace_old_places_with_ghost_vars(None, strengthening_spec.refinement_check_expr);
            let pos = self.register_error(
                strengthening_spec.spec_functions_span,
                ErrorCtxt::AssertMethodPostconditionStrengthening,
            );
            self.cfg_method.add_stmt(
                return_cfg_block,
                vir::Stmt::Assert(vir::Assert {
                    expr: patched_strengthening_spec,
                    position: pos,
                }),
            );
        }

        // Assert functional specification of postcondition
        self.cfg_method.add_stmt(
            return_cfg_block,
            vir::Stmt::comment("Assert functional specification of postcondition"),
        );
        let func_pos = self.register_error(self.mir.span, ErrorCtxt::AssertMethodPostcondition);
        let patched_func_spec = self.replace_old_places_with_ghost_vars(None, func_spec);
        self.cfg_method.add_stmt(
            return_cfg_block,
            vir::Stmt::Assert(vir::Assert {
                expr: patched_func_spec,
                position: func_pos,
            }),
        );

        // Assert type invariants
        self.cfg_method.add_stmt(
            return_cfg_block,
            vir::Stmt::comment("Assert type invariants"),
        );
        let patched_invs_spec = self.replace_old_places_with_ghost_vars(None, invs_spec);
        self.cfg_method.add_stmt(
            return_cfg_block,
            vir::Stmt::Assert(vir::Assert {
                expr: patched_invs_spec,
                position: type_inv_pos,
            }),
        );

        // Exhale permissions of postcondition
        self.cfg_method.add_stmt(
            return_cfg_block,
            vir::Stmt::comment("Exhale permissions of postcondition (1/3)"),
        );
        let perm_pos = self.register_error(self.mir.span, ErrorCtxt::ExhaleMethodPostcondition);
        let patched_type_spec = self.replace_old_places_with_ghost_vars(None, type_spec);
        debug_assert!(!perm_pos.is_default());
        self.cfg_method.add_stmt(
            return_cfg_block,
            vir::Stmt::Exhale(vir::Exhale {
                expr: patched_type_spec,
                position: perm_pos,
            }),
        );

        self.cfg_method.add_stmt(
            return_cfg_block,
            vir::Stmt::comment("Exhale permissions of postcondition (2/3)"),
        );
        if let Some(access) = return_type_spec {
            self.cfg_method.add_stmt(
                return_cfg_block,
                vir::Stmt::Exhale(vir::Exhale {
                    expr: access,
                    position: perm_pos,
                }),
            );
        }

        self.cfg_method.add_stmt(
            return_cfg_block,
            vir::Stmt::comment("Exhale permissions of postcondition (3/3)"),
        );
        for magic_wand in magic_wands {
            self.cfg_method.add_stmt(
                return_cfg_block,
                vir::Stmt::Exhale(vir::Exhale {
                    expr: magic_wand,
                    position: perm_pos,
                }),
            );
        }
        Ok(())
    }

    fn get_pure_var_for_preserving_value(
        &mut self,
        loop_head: BasicBlockIndex,
        place: &vir::Expr,
    ) -> vir::LocalVar {
        let loop_map = self
            .pure_var_for_preserving_value_map
            .get_mut(&loop_head)
            .unwrap();
        if let Some(local_var) = loop_map.get(place) {
            local_var.clone()
        } else {
            let mut counter = 0;
            let mut name = format!("_preserve${counter}");
            while self.auxiliary_local_vars.contains_key(&name) {
                counter += 1;
                name = format!("_preserve${counter}");
            }
            let vir_type = vir::Type::typed_ref("AuxRef");
            self.cfg_method.add_local_var(&name, vir_type.clone());
            self.auxiliary_local_vars
                .insert(name.clone(), vir_type.clone());
            let var = vir::LocalVar::new(name, vir_type);
            loop_map.insert(place.clone(), var.clone());
            var
        }
    }

    /// Since the loop invariant is taking all permission from the
    /// outer context, we need to preserve values of references by
    /// saving them in local variables.
    fn construct_value_preserving_equality(
        &mut self,
        loop_head: BasicBlockIndex,
        place: &vir::Expr,
    ) -> vir::Expr {
        let tmp_var = self.get_pure_var_for_preserving_value(loop_head, place);
        vir::Expr::BinOp(vir::BinOp {
            op_kind: vir::BinaryOpKind::EqCmp,
            left: Box::new(tmp_var.into()),
            right: Box::new(place.clone()),
            position: vir::Position::default(),
        })
    }

    fn construct_value_preserving_array_equality(
        &mut self,
        loop_head: BasicBlockIndex,
        array_base: vir::Expr,
    ) -> vir::Expr {
        // this label is inserted in encode_loop_invariant_exhale_stmts at the point
        // where the other "preserve equality" assignments are made
        use std::collections::hash_map::Entry::*;
        let old_label = match self.array_loop_old_label.entry(loop_head) {
            Occupied(lbl) => lbl.into_mut(),
            Vacant(v) => v.insert(self.cfg_method.get_fresh_label_name()),
        };

        let snap_array = vir::Expr::snap_app(array_base);
        let old_snap_array = vir::Expr::old(snap_array.clone(), old_label);
        vir_expr! { [snap_array] == [old_snap_array] }
    }

    /// Arguments:
    /// * `loop_head`: the loop head block, which identifies a loop.
    /// * `loop_inv`: the block at whose end the loop invariant should hold.
    /// * `drop_read_references`: should we add permissions to read
    ///   references? We drop permissions of read references from the
    ///   exhale before the loop and inhale after the loop so that
    ///   the knowledge about their values is not havocked.
    ///
    /// Result:
    /// * The first vector contains permissions.
    /// * The second vector contains value preserving equalities.
    #[tracing::instrument(level = "debug", skip(self))]
    fn encode_loop_invariant_permissions(
        &mut self,
        loop_head: BasicBlockIndex,
        loop_inv: BasicBlockIndex,
        drop_read_references: bool,
    ) -> EncodingResult<(Vec<vir::Expr>, Vec<vir::Expr>, Vec<vir::Expr>)> {
        let permissions_forest = self
            .loop_encoder
            .compute_loop_invariant(loop_head, loop_inv)
            .map_err(|err| match err {
                LoopAnalysisError::UnsupportedPlaceContext(place_ctxt, loc) => {
                    SpannedEncodingError::internal(
                        format!("loop uses the unexpected PlaceContext '{place_ctxt:?}'"),
                        self.mir_encoder.get_span_of_location(loc),
                    )
                }
            })?;
        debug!("permissions_forest: {:?}", permissions_forest);
        let loops = self.loop_encoder.get_enclosing_loop_heads(loop_head);
        let enclosing_permission_forest = if loops.len() > 1 {
            let next_to_last = loops.len() - 2;
            let enclosing_loop_head = loops[next_to_last];
            Some(
                self.loop_encoder
                    .compute_loop_invariant(
                        enclosing_loop_head,
                        self.cached_loop_invariant_block[&enclosing_loop_head],
                    )
                    .map_err(|err| match err {
                        LoopAnalysisError::UnsupportedPlaceContext(place_ctxt, loc) => {
                            SpannedEncodingError::internal(
                                format!("loop uses the unexpected PlaceContext '{place_ctxt:?}'"),
                                self.mir_encoder.get_span_of_location(loc),
                            )
                        }
                    })?,
            )
        } else {
            None
        };

        let mut permissions = Vec::new();
        let mut equalities = Vec::new();

        let mut array_pred_perms = FxHashMap::default();

        for tree in permissions_forest.get_trees().iter() {
            for (kind, mir_place) in tree.get_permissions().into_iter() {
                if kind.is_none() {
                    continue;
                }
                // we want to check if array or other place expr, so we call the mir_encoder
                // version of encode_place to avoid the postprocessing into statements
                let (encoded_place, ty, _) = self.mir_encoder.encode_place(mir_place)?;

                // NOTE: this catches array accesses to single indexes. we take the "max" of
                // none < read < write for the whole array, because we can't tell indices apart
                let (encoded_place, is_array_access) = match encoded_place.into_array_base() {
                    ExprOrArrayBase::Expr(e) => (e, false),
                    ExprOrArrayBase::ArrayBase(b) | ExprOrArrayBase::SliceBase(b) => (b, true),
                };

                debug!(
                    "kind={:?} mir_place={:?} encoded_place={:?} ty={:?}",
                    kind, mir_place, encoded_place, ty
                );
                match kind {
                    // Gives read permission to this node. It must not be a leaf node.
                    PermissionKind::ReadNode => {
                        if is_array_access {
                            // if it's already there, it's at least read -> nothing to do here
                            array_pred_perms
                                .entry(encoded_place)
                                .or_insert(vir::PermAmount::Read);
                        } else {
                            let perm =
                                vir::Expr::acc_permission(encoded_place, vir::PermAmount::Read);
                            permissions.push(perm);
                        }
                    }

                    // Gives write permission to this node. It must not be a leaf node.
                    PermissionKind::WriteNode => {
                        if is_array_access {
                            array_pred_perms.insert(encoded_place, vir::PermAmount::Write);
                        } else {
                            let perm =
                                vir::Expr::acc_permission(encoded_place, vir::PermAmount::Write);
                            permissions.push(perm);
                        }
                    }

                    // Gives read or write permission to the entire
                    // subtree including this node. This must be a leaf
                    // node.
                    PermissionKind::ReadSubtree | PermissionKind::WriteSubtree => {
                        let perm_amount = match kind {
                            PermissionKind::WriteSubtree => vir::PermAmount::Write,
                            PermissionKind::ReadSubtree => vir::PermAmount::Read,
                            _ => unreachable!(),
                        };
                        let def_init = self
                            .loop_encoder
                            .is_definitely_initialised(mir_place, loop_head);
                        debug!("    perm_amount={} def_init={}", perm_amount, def_init);
                        if let Some(base) =
                            utils::try_pop_deref(self.encoder.env().tcx(), mir_place)
                        {
                            // will panic if attempting to encode unsupported type
                            let ref_ty = self.mir_encoder.encode_place(base).unwrap().1;
                            match ref_ty.kind() {
                                ty::TyKind::RawPtr(ty::TypeAndMut { mutbl, .. })
                                | ty::TyKind::Ref(_, _, mutbl) => {
                                    if def_init {
                                        equalities.push(self.construct_value_preserving_equality(
                                            loop_head,
                                            &encoded_place,
                                        ));
                                    }
                                    if drop_read_references && mutbl == &Mutability::Not {
                                        continue;
                                    }
                                }
                                ref x => unreachable!("{:?}", x),
                            }
                        }
                        match ty.kind() {
                            ty::TyKind::Ref(_, ty, mutbl) => {
                                debug!(
                                    "encode_loop_invariant_permissions \
                                     mir_place={:?} mutability={:?} \
                                     drop_read_references={}",
                                    mir_place, mutbl, drop_read_references
                                );
                                // Use unfolded references.
                                let field = self.encoder.encode_dereference_field(*ty)?;
                                let field_place = encoded_place.field(field);
                                permissions.push(vir::Expr::acc_permission(
                                    field_place.clone(),
                                    perm_amount,
                                ));
                                if def_init {
                                    equalities.push(self.construct_value_preserving_equality(
                                        loop_head,
                                        &field_place,
                                    ));
                                }
                                if def_init && !(mutbl == &Mutability::Not && drop_read_references)
                                {
                                    permissions.push(
                                        vir::Expr::pred_permission(field_place, perm_amount)
                                            .unwrap(),
                                    );
                                }
                            }
                            _ => {
                                if is_array_access {
                                    array_pred_perms
                                        .entry(encoded_place)
                                        .and_modify(|e| {
                                            if perm_amount == vir::PermAmount::Write {
                                                *e = vir::PermAmount::Write;
                                            }
                                        })
                                        .or_insert(perm_amount);
                                } else {
                                    permissions.push(
                                        vir::Expr::pred_permission(encoded_place, perm_amount)
                                            .unwrap(),
                                    );
                                }

                                if let Some(forest) = &enclosing_permission_forest {
                                    for child_place in forest.get_children(mir_place) {
                                        // If the forest contains the place, but that place is a
                                        // regular node (either ReadNode or WriteNode), that means
                                        // that we will lose information about the children of that
                                        // place after the loop and we need to preserve it via local
                                        // variables.
                                        let encoded_child =
                                            self.mir_encoder.encode_place(child_place)?.0;
                                        match encoded_child.into_array_base() {
                                            ExprOrArrayBase::Expr(e) => {
                                                equalities.push(
                                                    self.construct_value_preserving_equality(
                                                        loop_head, &e,
                                                    ),
                                                );
                                            }
                                            ExprOrArrayBase::ArrayBase(b) => {
                                                let eq = self
                                                    .construct_value_preserving_array_equality(
                                                        loop_head, b,
                                                    );
                                                // arrays can be mentioned multiple times, so we
                                                // need to check here
                                                if !equalities.contains(&eq) {
                                                    equalities.push(eq);
                                                }
                                            }
                                            ExprOrArrayBase::SliceBase(_) => unimplemented!(
                                                "slices in loops not yet implemented"
                                            ),
                                        }
                                    }
                                }
                            }
                        }
                    }
                    // This should be repalced with WriteNode and
                    // WriteSubtree before this point.
                    PermissionKind::WriteNodeAndSubtree => unreachable!(),
                    // Give no permission to this node and the entire subtree. This
                    // must be a leaf node.
                    PermissionKind::None => unreachable!(),
                };
            }
        }

        // put the collected maxima of array permissions into the final permissions array
        // Note that array access permissions are always predicate permissions, never the raw
        // LocalVar
        trace!("array_pred_perms: {:?}", array_pred_perms);
        for (place, perm) in array_pred_perms.into_iter() {
            permissions.push(
                vir::Expr::pred_permission(place, perm).expect("invalid place in array_pred_perms"),
            );
        }

        // encode type invariants
        let mut invs_spec = Vec::new();
        for permission in &permissions {
            if let vir::Expr::PredicateAccessPredicate(vir::PredicateAccessPredicate {
                predicate_type,
                argument,
                ..
            }) = permission
            {
                let ty = self.encoder.decode_type_predicate_type(predicate_type)?;
                if !self.encoder.is_pure(self.proc_def_id, Some(self.substs)) {
                    let inv_func_app = self
                        .encoder
                        .encode_invariant_func_app(ty, (**argument).clone())?;
                    invs_spec.push(inv_func_app);
                }
            }
        }

        trace!(
            "[exit] encode_loop_invariant_permissions permissions={}",
            permissions.iter().fold(String::new(), |mut output, p| {
                let _ = write!(output, "{p}, ");
                output
            })
        );

        trace!(
            "[exit] encode_loop_invariant_permissions equalities={}",
            equalities.iter().fold(String::new(), |mut output, p| {
                let _ = write!(output, "{p}, ");
                output
            })
        );

        Ok((permissions, equalities, invs_spec))
    }

    /// Get the basic blocks that encode the specification of a loop invariant
    #[tracing::instrument(level = "debug", skip(self))]
    fn get_loop_spec_blocks(&self, loop_head: BasicBlockIndex) -> Vec<BasicBlockIndex> {
        let mut res = vec![];
        for bbi in self.procedure.get_reachable_cfg_blocks() {
            if Some(loop_head) == self.loop_encoder.get_loop_head(bbi)
                && self.procedure.is_spec_block(bbi)
            {
                res.push(bbi)
            } else {
                debug!(
                    "bbi {:?} has head {:?} and 'is spec' is {}",
                    bbi,
                    self.loop_encoder.get_loop_head(bbi),
                    self.procedure.is_spec_block(bbi)
                );
            }
        }
        res
    }

    /// Encode the functional specification of a loop
    #[tracing::instrument(level = "trace", skip(self), ret)]
    fn encode_loop_invariant_specs(
        &self,
        loop_head: BasicBlockIndex,
        _loop_inv_block: BasicBlockIndex,
    ) -> SpannedEncodingResult<(Vec<vir::Expr>, MultiSpan)> {
        let spec_blocks = self.get_loop_spec_blocks(loop_head);
        trace!(
            "loop head {:?} has spec blocks {:?}",
            loop_head,
            spec_blocks
        );

        // `body_invariant!(..)` is desugared to a closure with special attributes,
        // which we can detect and use to retrieve the specification.
        let mut encoded_specs = vec![];
        let mut encoded_spec_spans = vec![];
        for bbi in spec_blocks {
            for stmt in &self.mir.basic_blocks[bbi].statements {
                if let mir::StatementKind::Assign(box (
                    _,
                    mir::Rvalue::Aggregate(
                        box mir::AggregateKind::Closure(cl_def_id, cl_substs),
                        _,
                    ),
                )) = stmt.kind
                {
                    if let Some(spec) = self.encoder.get_loop_specs(cl_def_id) {
                        encoded_specs.push(self.encoder.encode_invariant(
                            self.mir,
                            bbi,
                            self.proc_def_id,
                            cl_substs,
                            true,
                        )?);
                        let invariant = match spec {
                            prusti_interface::specs::typed::LoopSpecification::Invariant(inv) => {
                                inv
                            }
                            _ => continue,
                        };
                        encoded_spec_spans.push(self.encoder.env().tcx().def_span(invariant));
                    }
                }
            }
        }
        Ok((encoded_specs, MultiSpan::from_spans(encoded_spec_spans)))
    }

    #[tracing::instrument(level = "trace", skip(self))]
    fn encode_loop_invariant_exhale_stmts(
        &mut self,
        loop_head: BasicBlockIndex,
        loop_inv_block: BasicBlockIndex,
        after_loop_iteration: bool,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        if !after_loop_iteration {
            self.pure_var_for_preserving_value_map
                .insert(loop_head, FxHashMap::default());
        }
        let (func_spec, func_spec_span) =
            self.encode_loop_invariant_specs(loop_head, loop_inv_block)?;
        let (permissions, equalities, invs_spec) = self
            .encode_loop_invariant_permissions(loop_head, loop_inv_block, true)
            .with_span(func_spec_span.clone())?;

        // TODO: use different positions, and generate different error messages, for the exhale
        // before the loop and after the loop body

        let assert_pos = self.register_error(
            // TODO: choose a proper error span
            func_spec_span.clone(),
            if after_loop_iteration {
                ErrorCtxt::AssertLoopInvariantAfterIteration
            } else {
                ErrorCtxt::AssertLoopInvariantOnEntry
            },
        );

        let exhale_pos = self.register_error(
            // TODO: choose a proper error span
            func_spec_span,
            if after_loop_iteration {
                ErrorCtxt::ExhaleLoopInvariantAfterIteration
            } else {
                ErrorCtxt::ExhaleLoopInvariantOnEntry
            },
        );

        let mut stmts = vec![vir::Stmt::comment(format!(
            "Assert and exhale the loop body invariant (loop head: {loop_head:?})"
        ))];
        if !after_loop_iteration {
            if let Some(label) = self.array_loop_old_label.get(&loop_head) {
                stmts.push(vir::Stmt::label(label));
            }
            for (place, field) in &self.pure_var_for_preserving_value_map[&loop_head] {
                stmts.push(vir::Stmt::Assign(vir::Assign {
                    target: field.into(),
                    source: place.clone(),
                    kind: vir::AssignKind::Ghost,
                }));
            }
        }
        assert!(!assert_pos.is_default());
        let obtain_predicates = permissions.iter().map(|p| {
            vir::Stmt::Obtain(vir::Obtain {
                expr: p.clone(),
                position: assert_pos,
            }) // TODO: Use a better position.
        });
        stmts.extend(obtain_predicates);

        stmts.push(vir::Stmt::Assert(vir::Assert {
            expr: func_spec.into_iter().conjoin(),
            position: assert_pos,
        }));
        stmts.push(vir::Stmt::Assert(vir::Assert {
            expr: invs_spec.into_iter().conjoin(),
            position: exhale_pos,
        }));
        let equalities_expr = equalities.into_iter().conjoin();
        stmts.push(vir::Stmt::Assert(vir::Assert {
            expr: equalities_expr,
            position: exhale_pos,
        }));
        let permission_expr = permissions.into_iter().conjoin();
        stmts.push(vir::Stmt::Exhale(vir::Exhale {
            expr: permission_expr,
            position: exhale_pos,
        }));
        Ok(stmts)
    }

    #[tracing::instrument(level = "trace", skip(self))]
    fn encode_loop_invariant_inhale_perm_stmts(
        &mut self,
        loop_head: BasicBlockIndex,
        loop_inv_block: BasicBlockIndex,
        after_loop: bool,
    ) -> EncodingResult<Vec<vir::Stmt>> {
        let (permissions, equalities, invs_spec) =
            self.encode_loop_invariant_permissions(loop_head, loop_inv_block, true)?;

        let permission_expr = permissions.into_iter().conjoin();
        let equality_expr = equalities.into_iter().conjoin();

        let mut stmts = vec![vir::Stmt::comment(format!(
            "Inhale the loop permissions invariant of block {loop_head:?}"
        ))];
        stmts.push(vir::Stmt::Inhale(vir::Inhale {
            expr: permission_expr,
        }));
        stmts.push(vir::Stmt::Inhale(vir::Inhale {
            expr: equality_expr,
        }));
        stmts.push(vir::Stmt::Inhale(vir::Inhale {
            expr: invs_spec.into_iter().conjoin(),
        }));
        Ok(stmts)
    }

    #[tracing::instrument(level = "trace", skip(self))]
    fn encode_loop_invariant_inhale_fnspec_stmts(
        &mut self,
        loop_head: BasicBlockIndex,
        loop_inv_block: BasicBlockIndex,
        after_loop: bool,
    ) -> SpannedEncodingResult<(Vec<vir::Stmt>, MultiSpan)> {
        let (func_spec, func_spec_span) =
            self.encode_loop_invariant_specs(loop_head, loop_inv_block)?;

        let mut stmts = vec![vir::Stmt::comment(format!(
            "Inhale the loop fnspec invariant of block {loop_head:?}"
        ))];
        stmts.push(vir::Stmt::Inhale(vir::Inhale {
            expr: func_spec.into_iter().conjoin(),
        }));
        Ok((stmts, func_spec_span))
    }

    fn encode_prusti_local(&self, local: Local) -> vir::LocalVar {
        let var_name = self.locals.get_name(local);
        let typ = self
            .encoder
            .encode_type(self.locals.get_type(local))
            .unwrap(); // will panic if attempting to encode unsupported type
        vir::LocalVar::new(var_name, typ)
    }

    // /// Returns
    // /// - `vir::Expr`: the place of the projection;
    // /// - `ty::Ty<'tcx>`: the type of the place;
    // /// - `Option<usize>`: optionally, the variant of the enum.
    // fn encode_projection(
    //     &self,
    //     index: usize,
    //     place: mir::Place<'tcx>,
    //     root: Option<Local>,
    // ) -> (vir::Expr, ty::Ty<'tcx>, Option<usize>) {
    //     debug!("Encode projection {} {:?} {:?}", index, place, root);
    //     let encoded_place = self.encode_place_with_subst_root(&place_projection.base, root);
    //     self.mir_encoder
    //         .encode_projection(index, place, Some(encoded_place))
    // }

    /// `containing_def_id` – MIR body in which the place is defined. `location`
    /// `location` – MIR terminator that makes the function call. If None,
    /// then we assume that `containing_def_id` is local.
    fn encode_generic_place(
        &self,
        containing_def_id: prusti_rustc_interface::hir::def_id::DefId,
        location: Option<mir::Location>,
        place: Place<'tcx>,
    ) -> EncodingResult<(vir::Expr, ty::Ty<'tcx>, Option<usize>)> {
        let mir_encoder = if let Some(location) = location {
            let block = &self.mir.basic_blocks[location.block];
            assert_eq!(
                block.statements.len(),
                location.statement_index,
                "expected terminator location"
            );
            match &block.terminator().kind {
                mir::TerminatorKind::Call {
                    args, destination, ..
                } => {
                    let tcx = self.encoder.env().tcx();
                    let arg_tys = args.iter().map(|arg| arg.ty(self.mir, tcx)).collect();
                    let return_ty = destination.ty(self.mir, tcx).ty;
                    FakeMirEncoder::new(self.encoder, arg_tys, return_ty)
                }
                kind => unreachable!("Only calls are expected. Found: {:?}", kind),
            }
        } else {
            // FIXME: why are we getting the MIR body for this?
            let mir = self
                .encoder
                .env()
                .body
                .get_impure_fn_body_identity(containing_def_id.expect_local());
            let return_ty = mir.return_ty();
            let arg_tys = mir.args_iter().map(|arg| mir.local_decls[arg].ty).collect();
            FakeMirEncoder::new(self.encoder, arg_tys, return_ty)
        };
        match place {
            Place::NormalPlace(place) => {
                let (pl, ty, var) = mir_encoder.encode_place(place)?;
                Ok((pl.try_into_expr()?, ty, var))
            }
            Place::SubstitutedPlace {
                substituted_root,
                place,
            } => {
                let (place_encoding, ty, variant) = mir_encoder.encode_place(place)?;
                let expr = place_encoding.try_into_expr()?;
                let new_root = self.encode_prusti_local(substituted_root);
                struct RootReplacer {
                    new_root: vir::LocalVar,
                }
                use vir::ExprFolder;
                impl ExprFolder for RootReplacer {
                    fn fold_local(&mut self, vir::Local { position, .. }: vir::Local) -> vir::Expr {
                        vir::Expr::local_with_pos(self.new_root.clone(), position)
                    }
                }
                Ok((RootReplacer { new_root }.fold(expr), ty, variant))
            }
        }
        // match place {
        //     &Place::NormalPlace(ref place) => self.encode_place_with_subst_root(place, None),
        //     &Place::SubstitutedPlace {
        //         substituted_root,
        //         ref place,
        //     } => self.encode_place_with_subst_root(place, Some(substituted_root)),
        // }
    }

    // /// Returns
    // /// - `vir::Expr`: the expression of the projection;
    // /// - `ty::Ty<'tcx>`: the type of the expression;
    // /// - `Option<usize>`: optionally, the variant of the enum.
    // fn encode_place_with_subst_root(
    //     &self,
    //     place: mir::Place<'tcx>,
    //     root: Option<Local>,
    // ) -> (vir::Expr, ty::Ty<'tcx>, Option<usize>) {
    //     if place.projection.is_empty() {
    //         let local = place.local;
    //         match root {
    //             Some(root) => (
    //                 self.encode_prusti_local(root).into(),
    //                 self.locals.get_type(root),
    //                 None,
    //             ),
    //             None => (
    //                 self.mir_encoder.encode_local(local)?.into(),
    //                 self.mir_encoder.get_local_ty(local),
    //                 None,
    //             )
    //         }
    //     } else {
    //         self.encode_projection(place_projection, root)
    //     }
    //     // match place {
    //     //     &mir::Place::Local(local) => match root {
    //     //         Some(root) => (
    //     //             self.encode_prusti_local(root).into(),
    //     //             self.locals.get_type(root),
    //     //             None,
    //     //         ),
    //     //         None => (
    //     //             self.mir_encoder.encode_local(local)?.into(),
    //     //             self.mir_encoder.get_local_ty(local),
    //     //             None,
    //     //         ),
    //     //     },
    //     //     &mir::Place::Projection(ref place_projection) => {
    //     //         self.encode_projection(place_projection, root)
    //     //     }
    //     //     x => unimplemented!("{:?}", x),
    //     // }
    // }

    /// Encode an assignment into an array without an intermediate temporary reference into the
    /// array.
    fn encode_array_direct_assign(
        &mut self,
        base: PlaceEncoding<'tcx>,
        index: vir::Expr,
        array_ty: ty::Ty<'tcx>,
        rhs: &mir::Rvalue<'tcx>,
        location: mir::Location,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        let span = self.mir_encoder.get_span_of_location(location);

        // We can't just inhale lookup_pure(base, index) == new_val, because that would
        // add conflicting info with the previous state of the array at that index.
        // So the idea is
        //   label lbl;
        //   exhale array;
        //   inhale array;
        //   // now all info about the array is `havoc`ed
        //   inhale forall i:: i != index ==> lookup_pure(array, i) == old[lbl](lookup_pure(array, i))
        //   inhale lookup_pure(array, index) == encoded_rhs
        //   // now we have all the contents as before, just one item updated

        let (encoded_array, mut stmts) = self
            .postprocess_place_encoding(
                base,
                ArrayAccessKind::Shared, // shouldn't be nested, so doesn't matter[tm]
            )
            .with_span(span)?;

        let label = self.cfg_method.get_fresh_label_name();
        stmts.push(vir::Stmt::label(&label));

        let sequence_types = self
            .encoder
            .encode_sequence_types(array_ty)
            .with_span(span)?;
        let sequence_len = sequence_types.len(self.encoder, encoded_array.clone());

        let array_acc_expr = vir::Expr::predicate_access_predicate(
            sequence_types.sequence_pred_type.clone(),
            encoded_array.clone(),
            vir::PermAmount::Write,
        );

        // exhale and re-inhale to havoc
        stmts.push(vir_stmt! { exhale [array_acc_expr] });
        stmts.push(vir_stmt! { inhale [array_acc_expr] });

        let old = |e| vir::Expr::labelled_old(&label, e);

        // For sequences with fixed len (e.g. arrays) this will be Some
        if sequence_types.sequence_len.is_none() {
            // inhale that len unchanged
            let len_eq = vir_expr! { [ sequence_len ] == [ old(sequence_len.clone()) ] };
            stmts.push(vir_stmt! { inhale [len_eq] });
        }

        let idx_val_int = self
            .encoder
            .patch_snapshots(vir::Expr::snap_app(index))
            .with_span(span)?;

        // inhale infos about array contents back
        let i_var: vir::Expr = vir_local! { i: Int }.into();
        let zero_le_i = vir_expr! { [vir::Expr::from(0usize)] <= [ i_var ] };
        let i_lt_len = vir_expr! { [ i_var ] < [ sequence_len ] };
        let i_ne_idx = vir_expr! { [ i_var ] != [ old(idx_val_int.clone()) ] };
        let idx_conditions = vir_expr! { [zero_le_i] && ([i_lt_len] && [i_ne_idx]) };
        let lookup_ret_ty = self
            .encoder
            .encode_snapshot_type(sequence_types.elem_ty_rs)
            .with_span(span)?;
        let lookup_array_i = sequence_types.encode_lookup_pure_call(
            self.encoder,
            encoded_array.clone(),
            i_var.clone(),
            lookup_ret_ty.clone(),
        );
        // FIXME: using `old` here is a work-around for https://github.com/viperproject/prusti-dev/issues/877
        // FIXME: which is due to an issue in Silicon, see https://github.com/viperproject/silicon/issues/603
        let lookup_array_i_old = sequence_types.encode_lookup_pure_call(
            self.encoder,
            old(encoded_array.clone()),
            i_var,
            lookup_ret_ty.clone(),
        );
        let lookup_same_as_old = vir_expr! { [lookup_array_i] == [old(lookup_array_i)] };
        let forall_body = vir_expr! { [idx_conditions] ==> [lookup_same_as_old] };
        let all_others_unchanged =
            vir_expr! { forall i: Int :: { [lookup_array_i_old] } :: [ forall_body ] };

        stmts.push(vir_stmt! { inhale [ all_others_unchanged ]});

        let tmp = vir::Expr::from(
            self.cfg_method
                .add_fresh_local_var(sequence_types.elem_pred_type.clone()),
        );
        stmts.extend(
            self.encode_assign(tmp.clone(), rhs, sequence_types.elem_ty_rs, location)
                .with_span(span)?,
        );

        let tmp_val_field = self
            .encoder
            .encode_value_expr(tmp, sequence_types.elem_ty_rs)
            .with_span(span)?;

        let indexed_lookup_pure_call = sequence_types.encode_lookup_pure_call(
            self.encoder,
            encoded_array,
            old(idx_val_int),
            lookup_ret_ty,
        );
        let indexed_updated =
            vir_expr! { [ indexed_lookup_pure_call ] == [ vir::Expr::snap_app(tmp_val_field) ] };

        stmts.push(vir_stmt! { inhale [ indexed_updated ] });

        Ok(stmts)
    }

    /// Return type:
    /// - `Vec<vir::Stmt>`: the statements that encode the assignment of `operand` to `lhs`
    #[tracing::instrument(level = "debug", skip(self), ret())]
    fn encode_assign_operand(
        &mut self,
        lhs: &vir::Expr,
        operand: &mir::Operand<'tcx>,
        location: mir::Location,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        let span = self.mir_encoder.get_span_of_location(location);
        let stmts = match operand {
            mir::Operand::Move(place) => {
                let (src, mut stmts, ty, _) =
                    self.encode_place(*place, ArrayAccessKind::Shared, location)?;
                let encode_stmts = match ty.kind() {
                    ty::TyKind::RawPtr(..) | ty::TyKind::Ref(..) => {
                        // Reborrow.
                        let field = self.encoder.encode_value_field(ty).with_span(span)?;
                        let mut alloc_stmts = self.prepare_assign_target(
                            lhs.clone(),
                            field.clone(),
                            location,
                            vir::AssignKind::Move,
                            false,
                        )?;
                        alloc_stmts.push(vir::Stmt::Assign(vir::Assign {
                            target: lhs.clone().field(field.clone()),
                            source: src.field(field),
                            kind: vir::AssignKind::Move,
                        }));
                        alloc_stmts
                    }
                    _ if config::enable_purification_optimization()
                        && prusti_common::vir::optimizations::purification::is_purifiable_type(
                            lhs.get_type(),
                        ) =>
                    {
                        self.encode_copy2(src, lhs.clone(), ty, location)?
                    }
                    _ => {
                        // Just move.
                        let move_assign = vir::Stmt::Assign(vir::Assign {
                            target: lhs.clone(),
                            source: src,
                            kind: vir::AssignKind::Move,
                        });
                        vec![move_assign]
                    }
                };

                stmts.extend(encode_stmts);

                // Store a label for this state
                let label = self.cfg_method.get_fresh_label_name();
                debug!("Current loc {:?} has label {}", location, label);
                self.label_after_location.insert(location, label.clone());
                stmts.push(vir::Stmt::label(label));

                stmts
            }

            mir::Operand::Copy(place) => {
                let (src, mut stmts, ty, _) =
                    self.encode_place(*place, ArrayAccessKind::Shared, location)?;
                let encode_stmts = match ty.kind() {
                    ty::TyKind::RawPtr(..) => {
                        return Err(SpannedEncodingError::unsupported(
                            "raw pointers are not supported",
                            span,
                        ));
                    }
                    ty::TyKind::Ref(..) => {
                        let loan = self.polonius_info().get_loan_at_location(location);
                        let ref_field = self.encoder.encode_value_field(ty).with_span(span)?;
                        let mut stmts = self.prepare_assign_target(
                            lhs.clone(),
                            ref_field.clone(),
                            location,
                            vir::AssignKind::SharedBorrow(loan.index().into()),
                            false,
                        )?;
                        stmts.push(vir::Stmt::Assign(vir::Assign {
                            target: lhs.clone().field(ref_field.clone()),
                            source: src.field(ref_field),
                            kind: vir::AssignKind::SharedBorrow(loan.index().into()),
                        }));
                        stmts
                    }
                    _ => self.encode_copy2(src, lhs.clone(), ty, location)?,
                };

                stmts.extend(encode_stmts);

                // Store a label for this state
                let label = self.cfg_method.get_fresh_label_name();
                debug!("Current loc {:?} has label {}", location, label);
                self.label_after_location.insert(location, label.clone());
                stmts.push(vir::Stmt::label(label));

                stmts
            }

            mir::Operand::Constant(expr) => {
                let ty = expr.ty();
                match ty.kind() {
                    ty::TyKind::Tuple(elements) if elements.is_empty() => Vec::new(),
                    _ => {
                        let field = self.encoder.encode_value_field(ty).with_span(span)?;
                        let mut stmts = self.prepare_assign_target(
                            lhs.clone(),
                            field.clone(),
                            location,
                            vir::AssignKind::Copy,
                            true,
                        )?;
                        // TODO Encoding of string literals is not yet supported,
                        // so do not encode an assignment if the RHS is a string
                        if !is_str(ty) {
                            // Initialize the constant
                            let const_val = self
                                .encoder
                                .encode_const_expr(ty, expr.literal)
                                .with_span(span)?;
                            // Initialize value of lhs
                            stmts.push(vir::Stmt::Assign(vir::Assign {
                                target: lhs.clone().field(field),
                                source: const_val,
                                kind: vir::AssignKind::Copy,
                            }));
                        }
                        stmts
                    }
                }
            }
        };
        debug!(
            "encode_assign_operand result: {}",
            vir::stmts_to_str(&stmts)
        );
        Ok(stmts)
    }

    /// Assignment with a binary operation on the RHS
    /// [encoded_lhs] = [left] [op] [right]
    #[tracing::instrument(level = "trace", skip(self))]
    fn encode_assign_binary_op(
        &mut self,
        op: mir::BinOp,
        left: &mir::Operand<'tcx>,
        right: &mir::Operand<'tcx>,
        encoded_lhs: vir::Expr,
        ty: ty::Ty<'tcx>,
        location: mir::Location,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        let span = self.mir_encoder.get_span_of_location(location);
        let encoded_left = self.mir_encoder.encode_operand_expr(left).with_span(span)?;
        let encoded_right = self
            .mir_encoder
            .encode_operand_expr(right)
            .with_span(span)?;
        let encoded_value = self
            .mir_encoder
            .encode_bin_op_expr(op, encoded_left, encoded_right, ty)
            .with_span(span)?;
        self.encode_copy_value_assign(encoded_lhs, encoded_value, ty, location)
    }

    fn encode_copy_value_assign(
        &mut self,
        encoded_lhs: vir::Expr,
        encoded_rhs: vir::Expr,
        ty: ty::Ty<'tcx>,
        location: mir::Location,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        let span = self.mir_encoder.get_span_of_location(location);
        let field = self.encoder.encode_value_field(ty).with_span(span)?;
        self.encode_copy_value_assign2(encoded_lhs, encoded_rhs, field, location)
    }

    /// Assignment with a(n overflow-)checked binary operation on the RHS.
    /// [encoded_lhs] = [left] [op] [right]
    #[tracing::instrument(level = "trace", skip(self))]
    fn encode_assign_checked_binary_op(
        &mut self,
        op: mir::BinOp,
        left: &mir::Operand<'tcx>,
        right: &mir::Operand<'tcx>,
        encoded_lhs: vir::Expr,
        ty: ty::Ty<'tcx>,
        location: mir::Location,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        let span = self.mir_encoder.get_span_of_location(location);
        let operand_ty = if let ty::TyKind::Tuple(types) = ty.kind() {
            types[0]
        } else {
            unreachable!()
        };
        let encoded_left = self.mir_encoder.encode_operand_expr(left).with_span(span)?;
        let encoded_right = self
            .mir_encoder
            .encode_operand_expr(right)
            .with_span(span)?;
        let encoded_value = self
            .mir_encoder
            .encode_bin_op_expr(op, encoded_left.clone(), encoded_right.clone(), operand_ty)
            .with_span(span)?;
        let encoded_check = self
            .mir_encoder
            .encode_bin_op_check(op, encoded_left, encoded_right, operand_ty)
            .with_span(span)?;
        let field_types = if let ty::TyKind::Tuple(ref x) = ty.kind() {
            x
        } else {
            unreachable!()
        };
        let value_field = self
            .encoder
            .encode_raw_ref_field("tuple_0".to_string(), field_types[0])
            .with_span(span)?;
        let value_field_value = self
            .encoder
            .encode_value_field(field_types[0])
            .with_span(span)?;
        let check_field = self
            .encoder
            .encode_raw_ref_field("tuple_1".to_string(), field_types[1])
            .with_span(span)?;
        let check_field_value = self
            .encoder
            .encode_value_field(field_types[1])
            .with_span(span)?;
        let mut stmts = if !self
            .init_info
            .is_vir_place_accessible(&encoded_lhs, location)
        {
            let mut alloc_stmts = self.encode_havoc(&encoded_lhs).with_span(span)?;
            let mut inhale_acc = |place| {
                alloc_stmts.push(vir::Stmt::Inhale(vir::Inhale {
                    expr: vir::Expr::acc_permission(place, vir::PermAmount::Write),
                }));
            };
            inhale_acc(encoded_lhs.clone().field(value_field.clone()));
            inhale_acc(
                encoded_lhs
                    .clone()
                    .field(value_field.clone())
                    .field(value_field_value.clone()),
            );
            inhale_acc(encoded_lhs.clone().field(check_field.clone()));
            inhale_acc(
                encoded_lhs
                    .clone()
                    .field(check_field.clone())
                    .field(check_field_value.clone()),
            );
            alloc_stmts
        } else {
            Vec::with_capacity(2)
        };
        // Initialize lhs.field
        stmts.push(vir::Stmt::Assign(vir::Assign {
            target: encoded_lhs
                .clone()
                .field(value_field)
                .field(value_field_value),
            source: encoded_value,
            kind: vir::AssignKind::Copy,
        }));
        stmts.push(vir::Stmt::Assign(vir::Assign {
            target: encoded_lhs.field(check_field).field(check_field_value),
            source: encoded_check,
            kind: vir::AssignKind::Copy,
        }));
        Ok(stmts)
    }

    /// Assignment with unary op as RHS.
    /// Unary ops currently are logical and arithmetic negation
    /// [encoded_lhs] = [op] [operand]
    #[tracing::instrument(level = "trace", skip(self))]
    fn encode_assign_unary_op(
        &mut self,
        op: mir::UnOp,
        operand: &mir::Operand<'tcx>,
        encoded_lhs: vir::Expr,
        ty: ty::Ty<'tcx>,
        location: mir::Location,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        let encoded_val = self
            .mir_encoder
            .encode_operand_expr(operand)
            .with_span(self.mir_encoder.get_span_of_location(location))?;
        let encoded_value = self.mir_encoder.encode_unary_op_expr(op, encoded_val);
        // Initialize `lhs.field`
        self.encode_copy_value_assign(encoded_lhs, encoded_value, ty, location)
    }

    /// Assignment with a nullary op on the RHS.
    /// Nullary ops currently are sizeof and alignof.
    /// [lhs] = [op] [op_ty]
    #[tracing::instrument(level = "trace", skip(self))]
    fn encode_assign_nullary_op(
        &mut self,
        op: &mir::NullOp,
        op_ty: ty::Ty<'tcx>,
        encoded_lhs: vir::Expr,
        ty: ty::Ty<'tcx>,
        location: mir::Location,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        let tcx = self.encoder.env().tcx();
        let param_env = tcx.param_env(self.proc_def_id);
        let layout = match tcx.layout_of(param_env.and(op_ty)) {
            Ok(layout_of) => layout_of.layout,
            Err(_) => {
                return Err(SpannedEncodingError::internal(
                    format!("could not fetch layout of type `{op_ty}` while translating `{op:?}`"),
                    self.mir.source_info(location).span,
                ))
            }
        };
        let bytes = match op {
            mir::NullOp::SizeOf => layout.size().bytes(),
            // FIXME: abi or pref?
            mir::NullOp::AlignOf => layout.align().abi.bytes(),
            mir::NullOp::OffsetOf(_) => {
                return Err(SpannedEncodingError::internal(
                    "`OffsetOf` is not supported yet".to_string(),
                    self.mir.source_info(location).span,
                ))
            }
        };
        let bytes_vir = vir::Expr::from(bytes);
        self.encode_copy_value_assign(encoded_lhs, bytes_vir, ty, location)
    }

    fn encode_assign_box(
        &mut self,
        op_ty: ty::Ty<'tcx>,
        encoded_lhs: vir::Expr,
        ty: ty::Ty<'tcx>,
        location: mir::Location,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        assert_eq!(op_ty, ty.boxed_ty());
        let span = self.mir_encoder.get_span_of_location(location);
        let ref_field = self
            .encoder
            .encode_dereference_field(op_ty)
            .with_span(self.mir_encoder.get_span_of_location(location))?;
        let box_content = encoded_lhs.clone().field(ref_field.clone());

        let mut stmts = self.prepare_assign_target(
            encoded_lhs,
            ref_field,
            location,
            vir::AssignKind::Move,
            false,
        )?;

        // Allocate `box_content`
        // TODO: This is also encoding initialization, which should be avoided because both
        //   `Rvalue::NullaryOp(NullOp::Box)` and `Rvalue::ShallowInitBox` don't initialize the
        //   content of the box.
        stmts.extend(
            self.encode_havoc_and_initialization(&box_content)
                .with_span(span)?,
        );

        // Leave `box_content` uninitialized
        Ok(stmts)
    }

    /// Assignment with the RHS being the discriminant value of an enum
    /// [lhs] = discriminant of [src]
    #[tracing::instrument(level = "debug", skip(self))]
    fn encode_assign_discriminant(
        &mut self,
        src: mir::Place<'tcx>,
        location: mir::Location,
        encoded_lhs: vir::Expr,
        ty: ty::Ty<'tcx>,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        let span = self.mir_encoder.get_span_of_location(location);
        let (encoded_src, mut stmts, src_ty, _) =
            self.encode_place(src, ArrayAccessKind::Shared, location)?;
        let encode_stmts = match src_ty.kind() {
            ty::TyKind::Adt(adt_def, _) if !adt_def.is_box() => {
                let num_variants = adt_def.variants().len();
                // Initialize `lhs.int_field`
                // Note: in our encoding an enumeration with just one variant has
                // no discriminant
                if num_variants > 1 {
                    // remember where discriminant can be found for counterexamples
                    if config::counterexample() {
                        let enum_id = encoded_src.to_string();
                        self.encoder.add_discriminant_info(
                            enum_id,
                            encoded_lhs.to_string(),
                            self.proc_def_id,
                        );
                    }
                    let encoded_rhs = self
                        .encoder
                        .encode_discriminant_func_app(encoded_src, *adt_def)?;
                    self.encode_copy_value_assign(encoded_lhs, encoded_rhs, ty, location)?
                } else {
                    vec![]
                }
            }

            ty::TyKind::Int(_) | ty::TyKind::Uint(_) | ty::TyKind::Float(_) => {
                let value_field = self.encoder.encode_value_field(src_ty).with_span(span)?;
                let discr_value = encoded_src.field(value_field);
                self.encode_copy_value_assign(encoded_lhs, discr_value, ty, location)?
            }

            ref x => {
                debug!("The discriminant of type {:?} is not defined", x);
                vec![]
            }
        };
        stmts.extend(encode_stmts);
        Ok(stmts)
    }

    /// Assignment with the RHS being referenced
    /// [encoded_lhs] = &[mir_borrow_kind] [place]
    #[tracing::instrument(level = "debug", skip(self))]
    fn encode_assign_ref(
        &mut self,
        mir_borrow_kind: mir::BorrowKind,
        place: mir::Place<'tcx>,
        location: mir::Location,
        encoded_lhs: vir::Expr,
        ty: ty::Ty<'tcx>,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        let span = self.mir_encoder.get_span_of_location(location);
        let loan = self.polonius_info().get_loan_at_location(location);
        let (vir_assign_kind, array_encode_kind) = match mir_borrow_kind {
            mir::BorrowKind::Shared => (
                vir::AssignKind::SharedBorrow(loan.index().into()),
                ArrayAccessKind::Shared,
            ),
            mir::BorrowKind::Mut { .. } => (
                vir::AssignKind::MutableBorrow(loan.index().into()),
                ArrayAccessKind::Mutable(Some(loan.index().into()), location),
            ),
            _ => return Err(Self::unsupported_borrow_kind(mir_borrow_kind).with_span(span)),
        };
        let (encoded_value, mut stmts, _, _) =
            self.encode_place(place, array_encode_kind, location)?;
        // Initialize ref_var.ref_field
        let field = self.encoder.encode_value_field(ty).with_span(span)?;
        stmts.extend(self.prepare_assign_target(
            encoded_lhs.clone(),
            field.clone(),
            location,
            vir_assign_kind,
            false,
        )?);
        stmts.push(vir::Stmt::Assign(vir::Assign {
            target: encoded_lhs.field(field),
            source: encoded_value,
            kind: vir_assign_kind,
        }));
        // Store a label for this state
        let label = self.cfg_method.get_fresh_label_name();
        debug!("Current loc {:?} has label {}", location, label);
        self.label_after_location.insert(location, label.clone());
        stmts.push(vir::Stmt::label(label));
        Ok(stmts)
    }

    /// Assignment where the RHS is a cast operation
    /// [encoded_lhs] = [operand] as [dst_ty]
    #[tracing::instrument(level = "trace", skip(self))]
    fn encode_cast(
        &mut self,
        operand: &mir::Operand<'tcx>,
        dst_ty: ty::Ty<'tcx>,
        encoded_lhs: vir::Expr,
        ty: ty::Ty<'tcx>,
        location: mir::Location,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        let span = self.mir_encoder.get_span_of_location(location);
        let encoded_val = self.mir_encoder.encode_cast_expr(operand, dst_ty, span)?;
        self.encode_copy_value_assign(encoded_lhs, encoded_val, ty, location)
    }

    /// Take a slice into the RHS array
    /// (also happens for calls that you do on an array that are slice methods, like .len())
    #[tracing::instrument(level = "debug", skip(self))]
    fn encode_assign_slice(
        &mut self,
        encoded_lhs: vir::Expr,
        operand: &mir::Operand<'tcx>,
        ty: ty::Ty<'tcx>,
        location: mir::Location,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        debug_assert!(ty.is_slice_ref());
        let span = self.mir_encoder.get_span_of_location(location);
        let mut stmts = Vec::new();

        let label = self.cfg_method.get_fresh_label_name();
        stmts.push(vir::Stmt::label(label.clone()));

        let (slice_ty, is_mut) = if let ty::TyKind::Ref(_, slice_ty, m) = ty.kind() {
            (slice_ty, m == &mir::Mutability::Mut)
        } else {
            unreachable!("encode_assign_slice on a non-ref?!")
        };
        let slice_types = self
            .encoder
            .encode_sequence_types(*slice_ty)
            .with_span(span)?;

        stmts.extend(self.encode_havoc(&encoded_lhs).with_span(span)?);
        let val_ref_field = self.encoder.encode_value_field(ty).with_span(span)?;
        let slice_expr = encoded_lhs.field(val_ref_field);
        stmts.push(
            vir_stmt! { inhale [vir::Expr::FieldAccessPredicate( vir::FieldAccessPredicate {
                base: Box::new(slice_expr.clone()),
                permission: vir::PermAmount::Write,
                position: vir::Position::default(),
            })]},
        );

        let slice_perm = vir::Expr::PredicateAccessPredicate(vir::PredicateAccessPredicate {
            predicate_type: slice_types.sequence_pred_type.clone(),
            argument: Box::new(slice_expr.clone()),
            permission: if is_mut {
                vir::PermAmount::Write
            } else {
                vir::PermAmount::Read
            },
            position: vir::Position::default(),
        });
        stmts.push(vir_stmt! { inhale [slice_perm] });

        let (rhs_place, rhs_ty) = if let mir::Operand::Move(place) = operand {
            let (rhs_place, rhs_ty, ..) = self.mir_encoder.encode_place(*place).with_span(span)?;
            (rhs_place.try_into_expr().with_span(span)?, rhs_ty)
        } else {
            unreachable!()
        };

        let rhs_array_ty = if let ty::TyKind::Ref(_, array_ty, _) = rhs_ty.kind() {
            array_ty
        } else {
            unreachable!("rhs array not a ref?")
        };

        let val_ref_field = self.encoder.encode_value_field(rhs_ty).with_span(span)?;
        let rhs_expr = rhs_place.field(val_ref_field);
        let sequence_types = self
            .encoder
            .encode_sequence_types(*rhs_array_ty)
            .with_span(span)?;

        let slice_len_call = slice_types.len(self.encoder, slice_expr.clone());

        stmts.push(vir::Stmt::Inhale( vir::Inhale {
            expr: vir_expr!{ [slice_len_call] == [sequence_types.len(self.encoder, rhs_expr.clone())] }
        }));

        let elem_snap_ty = self
            .encoder
            .encode_snapshot_type(sequence_types.elem_ty_rs)
            .with_span(span)?;

        let i: vir::Expr = vir_local! { i: Int }.into();

        let array_lookup_call = sequence_types.encode_lookup_pure_call(
            self.encoder,
            rhs_expr.clone(),
            i.clone(),
            elem_snap_ty.clone(),
        );

        let slice_lookup_call =
            slice_types.encode_lookup_pure_call(self.encoder, slice_expr, i.clone(), elem_snap_ty);

        let indices = vir_expr! { ([vir::Expr::from(0usize)] <= [i]) && ([i] < [sequence_types.len(self.encoder, rhs_expr)]) };

        stmts.push(vir::Stmt::Inhale(vir::Inhale {
            expr: vir_expr! {
            forall i: Int ::
            { [array_lookup_call] } { [slice_lookup_call] } ::
            ([indices] ==> ([array_lookup_call] == [slice_lookup_call])) },
        }));

        // Store a label for permissions got back from the call
        debug!(
            "Pure function call location {:?} has label {}",
            location, label
        );
        self.label_after_location.insert(location, label);

        Ok(stmts)
    }

    #[tracing::instrument(level = "trace", skip(self))]
    fn encode_assign_sequence_len(
        &mut self,
        encoded_lhs: vir::Expr,
        place: mir::Place<'tcx>,
        dst_ty: ty::Ty<'tcx>,
        location: mir::Location,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        let span = self.mir_encoder.get_span_of_location(location);
        let (encoded_place, mut stmts, place_ty, ..) =
            self.encode_place(place, ArrayAccessKind::Mutable(None, location), location)?;
        match place_ty.kind() {
            ty::TyKind::Array(..) | ty::TyKind::Slice(..) => {
                let slice_types = self
                    .encoder
                    .encode_sequence_types(place_ty)
                    .with_span(span)?;

                stmts.push(vir::Stmt::Assert(vir::Assert {
                    expr: vir::Expr::predicate_access_predicate(
                        slice_types.sequence_pred_type.clone(),
                        encoded_place.clone(),
                        vir::PermAmount::Read,
                    ),
                    position: vir::Position::default(),
                }));

                let rhs = slice_types.len(self.encoder, encoded_place);

                stmts.extend(self.encode_copy_value_assign(encoded_lhs, rhs, dst_ty, location)?);
            }
            other => {
                return Err(EncodingError::unsupported(format!(
                    "length operation on unsupported type '{other:?}'"
                ))
                .with_span(span))
            }
        }

        Ok(stmts)
    }

    fn encode_assign_array_repeat_initializer(
        &mut self,
        encoded_lhs: vir::Expr,
        operand: &mir::Operand<'tcx>,
        times: ty::Const<'tcx>,
        ty: ty::Ty<'tcx>,
        location: mir::Location,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        let span = self.mir_encoder.get_span_of_location(location);
        let sequence_types = self.encoder.encode_sequence_types(ty).with_span(span)?;

        let encoded_operand = self
            .mir_encoder
            .encode_operand_expr(operand)
            .with_span(span)?;
        let len: usize = self
            .encoder
            .const_eval_intlike(mir::ConstantKind::Ty(times))
            .with_span(span)?
            .to_u64()
            .unwrap()
            .try_into()
            .unwrap();
        let lookup_ret_ty = self
            .encoder
            .encode_snapshot_type(sequence_types.elem_ty_rs)
            .with_span(span)?;

        let inhaled_operand = if lookup_ret_ty.is_domain() || lookup_ret_ty.is_snapshot() {
            vir::Expr::snap_app(encoded_operand)
        } else {
            encoded_operand
        };

        let mut stmts = self
            .encode_havoc_and_initialization(&encoded_lhs)
            .with_span(span)?;
        let idx: vir::Expr = vir_local! { i: Int }.into();
        let indices =
            vir_expr! { ([vir::Expr::from(0usize)] <= [idx]) && ([idx] < [vir::Expr::from(len)]) };
        let lookup_pure_call =
            sequence_types.encode_lookup_pure_call(self.encoder, encoded_lhs, idx, lookup_ret_ty);
        stmts.push(vir::Stmt::Inhale(vir::Inhale {
            expr: vir_expr! {
            forall i: Int ::
            { [lookup_pure_call] } ::
            ([indices] ==> ([lookup_pure_call] == [inhaled_operand])) },
        }));

        Ok(stmts)
    }

    pub fn get_auxiliary_local_var(&mut self, suffix: &str, vir_type: vir::Type) -> vir::LocalVar {
        let name = format!("_aux_{}_{}", suffix, vir_type.name());
        if self.auxiliary_local_vars.contains_key(&name) {
            assert_eq!(self.auxiliary_local_vars[&name], vir_type);
        } else {
            self.cfg_method.add_local_var(&name, vir_type.clone());
            self.auxiliary_local_vars
                .insert(name.clone(), vir_type.clone());
        }
        vir::LocalVar::new(name, vir_type)
    }

    #[tracing::instrument(level = "debug", skip(self))]
    fn encode_havoc(&mut self, dst: &vir::Expr) -> EncodingResult<Vec<vir::Stmt>> {
        let havoc_ref_method_name = self
            .encoder
            .encode_builtin_method_use(BuiltinMethodKind::HavocRef)?;
        if let vir::Expr::Local(vir::Local {
            variable: ref dst_local_var,
            ..
        }) = dst
        {
            Ok(vec![vir::Stmt::MethodCall(vir::MethodCall {
                method_name: havoc_ref_method_name,
                arguments: vec![],
                targets: vec![dst_local_var.clone()],
            })])
        } else {
            let tmp_var = self.get_auxiliary_local_var("havoc", dst.get_type().clone());
            Ok(vec![
                vir::Stmt::MethodCall(vir::MethodCall {
                    method_name: havoc_ref_method_name,
                    arguments: vec![],
                    targets: vec![tmp_var.clone()],
                }),
                vir::Stmt::Assign(vir::Assign {
                    target: dst.clone(),
                    source: tmp_var.into(),
                    kind: vir::AssignKind::Move,
                }),
            ])
        }
    }

    /// Havoc and assume permission on fields
    #[tracing::instrument(level = "debug", skip(self))]
    fn encode_havoc_and_initialization(
        &mut self,
        dst: &vir::Expr,
    ) -> EncodingResult<Vec<vir::Stmt>> {
        let mut stmts = vec![];
        // Havoc `dst`
        stmts.extend(self.encode_havoc(dst)?);
        // Initialize `dst`
        stmts.push(vir::Stmt::Inhale(vir::Inhale {
            expr: self
                .mir_encoder
                .encode_place_predicate_permission(dst.clone(), vir::PermAmount::Write)
                .unwrap(),
        }));
        Ok(stmts)
    }

    /// Prepare the ``dst`` to be copy target:
    ///
    /// 1.  Havoc and allocate if it is not yet allocated.
    #[tracing::instrument(level = "debug", skip(self))]
    fn prepare_assign_target(
        &mut self,
        dst: vir::Expr,
        field: vir::Field,
        location: mir::Location,
        vir_assign_kind: vir::AssignKind,
        can_copy_reference: bool, // reference copies are allowed if the field is a constant
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        let span = self.mir_encoder.get_span_of_location(location);
        if !self.init_info.is_vir_place_accessible(&dst, location) {
            let mut alloc_stmts = self.encode_havoc(&dst).with_span(span)?;
            let dst_field = dst.clone().field(field.clone());
            let acc = vir::Expr::acc_permission(dst_field.clone(), vir::PermAmount::Write);
            alloc_stmts.push(vir::Stmt::Inhale(vir::Inhale { expr: acc }));
            match vir_assign_kind {
                vir::AssignKind::Copy => {
                    if field.typ.is_typed_ref_or_type_var() {
                        if can_copy_reference {
                            let pred_acc = vir::Expr::predicate_access_predicate(
                                field.typ,
                                dst_field,
                                vir::PermAmount::Read,
                            );
                            alloc_stmts.push(vir::Stmt::Inhale(vir::Inhale { expr: pred_acc }));
                        } else {
                            // TODO: Inhale the predicate rooted at dst_field
                            return Err(SpannedEncodingError::unsupported(
                                "the encoding of this reference copy has not \
                                been implemented",
                                self.mir_encoder.get_span_of_location(location),
                            ));
                        }
                    }
                }
                vir::AssignKind::Move
                | vir::AssignKind::MutableBorrow(_)
                | vir::AssignKind::SharedBorrow(_) => {}
                vir::AssignKind::Ghost => unreachable!(),
            }
            debug!("alloc_stmts = {}", alloc_stmts.iter().to_string());
            Ok(alloc_stmts)
        } else {
            Ok(Vec::with_capacity(1))
        }
    }

    /// Encode value copy assignment. Havoc and allocate the target if necessary.
    fn encode_copy_value_assign2(
        &mut self,
        lhs: vir::Expr,
        rhs: vir::Expr,
        field: vir::Field,
        location: mir::Location,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        let mut stmts = self.prepare_assign_target(
            lhs.clone(),
            field.clone(),
            location,
            vir::AssignKind::Copy,
            false,
        )?;
        stmts.push(vir::Stmt::Assign(vir::Assign {
            target: lhs.field(field),
            source: rhs,
            kind: vir::AssignKind::Copy,
        }));
        Ok(stmts)
    }

    /// Copy a primitive value such as an integer. Allocate the target
    /// if necessary.
    fn encode_copy_primitive_value(
        &mut self,
        src: vir::Expr,
        dst: vir::Expr,
        ty: ty::Ty<'tcx>,
        location: mir::Location,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        let span = self.mir_encoder.get_span_of_location(location);
        let field = self.encoder.encode_value_field(ty).with_span(span)?;
        self.encode_copy_value_assign2(dst, src.field(field.clone()), field, location)
    }

    /// Copy a value by inhaling snapshot equality.
    fn encode_copy_snapshot_value(
        &mut self,
        src: vir::Expr,
        dst: vir::Expr,
    ) -> EncodingResult<Vec<vir::Stmt>> {
        let mut stmts = self.encode_havoc_and_initialization(&dst)?;
        stmts.push(vir::Stmt::Inhale(vir::Inhale {
            expr: vir::Expr::eq_cmp(vir::Expr::snap_app(src), vir::Expr::snap_app(dst)),
        }));
        Ok(stmts)
    }

    fn encode_copy2(
        &mut self,
        src: vir::Expr,
        dst: vir::Expr,
        self_ty: ty::Ty<'tcx>,
        location: mir::Location,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        let span = self.mir_encoder.get_span_of_location(location);
        let stmts = match self_ty.kind() {
            ty::TyKind::Bool
            | ty::TyKind::Int(_)
            | ty::TyKind::Uint(_)
            | ty::TyKind::Float(_)
            | ty::TyKind::Char => self.encode_copy_primitive_value(src, dst, self_ty, location)?,

            ty::TyKind::Adt(_, _)
            | ty::TyKind::Closure(_, _)
            | ty::TyKind::Tuple(_)
            | ty::TyKind::Param(_)
            | ty::TyKind::Array(_, _) => {
                self.encode_copy_snapshot_value(src, dst).with_span(span)?
            }

            _ => {
                return Err(SpannedEncodingError::unsupported(
                    format!(
                        "copy operation for an unsupported type {:?}",
                        self_ty.kind()
                    ),
                    span,
                ));
            }
        };
        Ok(stmts)
    }

    /// Assignment with an aggregate on the RHS. Aggregates are e.g. arrays, structs, enums,
    /// tuples
    /// [dst] = Foo { x: [op_0], y: [op_1], .. }
    /// [dst] = [ op_0, op_1, ..];
    #[tracing::instrument(level = "debug", skip(self))]
    fn encode_assign_aggregate(
        &mut self,
        dst: &vir::Expr,
        ty: ty::Ty<'tcx>,
        aggregate: &mir::AggregateKind<'tcx>,
        operands: &IndexSlice<FieldIdx, mir::Operand<'tcx>>,
        location: mir::Location,
    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
        let span = self.mir_encoder.get_span_of_location(location);
        let mut stmts = self.encode_havoc_and_initialization(dst).with_span(span)?;
        // Initialize values
        match *aggregate {
            mir::AggregateKind::Tuple => {
                let field_types = if let ty::TyKind::Tuple(ref x) = ty.kind() {
                    x
                } else {
                    unreachable!()
                };
                for (field_num, operand) in operands.iter().enumerate() {
                    let field_name = format!("tuple_{field_num}");
                    let encoded_field = self
                        .encoder
                        .encode_raw_ref_field(field_name, field_types[field_num])
                        .with_span(span)?;
                    stmts.extend(self.encode_assign_operand(
                        &dst.clone().field(encoded_field),
                        operand,
                        location,
                    )?);
                }
            }

            mir::AggregateKind::Adt(adt_did, variant_index, subst, _, _) => {
                let tcx = self.encoder.env().tcx();
                let adt_def = tcx.adt_def(adt_did);
                if adt_def.is_union() {
                    return Err(SpannedEncodingError::unsupported(
                        "unions are not supported",
                        span,
                    ));
                }
                let num_variants = adt_def.variants().len();
                let variant_def = &adt_def.variants()[variant_index];
                let mut dst_base = dst.clone();
                if num_variants != 1 {
                    // An enum.
                    // Handle *signed* discriminats
                    let discr_type = adt_def.repr().discr_type();
                    let discr_value: vir::Expr = if discr_type.is_signed() {
                        let bit_size = Integer::from_attr(&tcx, discr_type).size().bits();
                        let shift = 128 - bit_size;
                        let unsigned_discr =
                            adt_def.discriminant_for_variant(tcx, variant_index).val;
                        let casted_discr = unsigned_discr as i128;
                        // sign extend the raw representation to be an i128
                        ((casted_discr << shift) >> shift).into()
                    } else {
                        adt_def
                            .discriminant_for_variant(tcx, variant_index)
                            .val
                            .into()
                    };
                    // dst was havocked, so it is safe to assume the equality here.
                    let discriminant = self
                        .encoder
                        .encode_discriminant_func_app(dst.clone(), adt_def)?;
                    stmts.push(vir::Stmt::Inhale(vir::Inhale {
                        expr: vir::Expr::eq_cmp(discriminant, discr_value),
                    }));

                    let variant_name = variant_def.ident(tcx).to_string();
                    let new_dst_base = dst_base.variant(&variant_name);
                    let variant_field = if let vir::Expr::Variant(vir::Variant {
                        variant_index: ref field,
                        ..
                    }) = new_dst_base
                    {
                        field.clone()
                    } else {
                        unreachable!()
                    };

                    if !variant_def.fields.is_empty() {
                        stmts.push(vir::Stmt::Downcast(vir::Downcast {
                            base: dst.clone(),
                            field: variant_field,
                        }));
                    }

                    dst_base = new_dst_base;
                }
                for (field_index, field) in variant_def.fields.iter().enumerate() {
                    let operand = &operands[field_index.into()];
                    let field_name = field.ident(tcx).to_string();
                    let field_ty = field.ty(tcx, subst);
                    let encoded_field = self
                        .encoder
                        .encode_struct_field(&field_name, field_ty)
                        .with_span(span)?;
                    stmts.extend(self.encode_assign_operand(
                        &dst_base.clone().field(encoded_field),
                        operand,
                        location,
                    )?);
                }
            }

            mir::AggregateKind::Closure(def_id, substs) => {
                // TODO: might need to assert history invariants?
                assert!(
                    !self.encoder.is_spec_closure(def_id),
                    "spec closure: {def_id:?}"
                );
                let cl_substs = substs.as_closure();
                for (field_index, field_ty) in cl_substs.upvar_tys().iter().enumerate() {
                    let operand = &operands[field_index.into()];
                    let field_name = format!("closure_{field_index}");
                    let encoded_field = self
                        .encoder
                        .encode_raw_ref_field(field_name, field_ty)
                        .with_span(span)?;
                    stmts.extend(self.encode_assign_operand(
                        &dst.clone().field(encoded_field),
                        operand,
                        location,
                    )?);
                }
            }

            mir::AggregateKind::Array(..) => {
                let sequence_types = self.encoder.encode_sequence_types(ty).with_span(span)?;
                let lookup_ret_ty = self
                    .encoder
                    .encode_snapshot_type(sequence_types.elem_ty_rs)
                    .with_span(span)?;

                for (idx, operand) in operands.iter().enumerate() {
                    let lookup_pure_call = sequence_types.encode_lookup_pure_call(
                        self.encoder,
                        dst.clone(),
                        idx.into(),
                        lookup_ret_ty.clone(),
                    );

                    let encoded_operand = self
                        .mir_encoder
                        .encode_operand_expr(operand)
                        .with_span(span)?;

                    stmts.push(
                        vir::Stmt::Inhale( vir::Inhale {
                            expr: vir_expr!{ [lookup_pure_call] == [vir::Expr::snap_app(encoded_operand)]},
                        }),
                    );
                }
            }

            mir::AggregateKind::Generator(..) => {
                return Err(SpannedEncodingError::unsupported(
                    "construction of generators is not supported",
                    span,
                ));
            }
        }

        Ok(stmts)
    }

    fn check_vir(&self) -> SpannedEncodingResult<()> {
        if self.cfg_method.has_loops() {
            return Err(SpannedEncodingError::internal(
                "The Viper encoding contains unexpected loops in the CFG",
                self.mir.span,
            ));
        }
        Ok(())
    }

    #[tracing::instrument(level = "debug", skip(self))]
    fn get_label_after_location(
        &mut self,
        location: mir::Location,
    ) -> SpannedEncodingResult<Option<&String>> {
        let opt_label = self.label_after_location.get(&location);
        if opt_label.is_none() {
            if config::allow_unreachable_unsupported_code() {
                // The encoding of unsupported code does not generate the expected labels
                debug!("Location {:?} has not yet been encoded", location);
            } else {
                // When no unsupported statements are allowed, a missing label is a bug.
                return Err(SpannedEncodingError::internal(
                    format!("Location {location:?} has not yet been encoded"),
                    self.mir_encoder.get_span_of_location(location),
                ));
            }
        }
        Ok(opt_label)
    }

    fn get_loop_span(&self, loop_head: mir::BasicBlock) -> Span {
        let loop_info = self.loop_encoder.loops();
        debug_assert!(loop_info.is_loop_head(loop_head));
        let loop_body = loop_info.get_loop_body(loop_head);
        let loop_head_span = self.mir_encoder.get_span_of_basic_block(loop_head);
        loop_body
            .iter()
            .map(|&bb| self.mir_encoder.get_span_of_basic_block(bb))
            .filter(|&span| span.contains(loop_head_span))
            .min()
            .unwrap()
    }

    /// A local version of encode_place
    #[tracing::instrument(level = "trace", skip(self))]
    fn encode_place(
        &mut self,
        place: mir::Place<'tcx>,
        encode_kind: ArrayAccessKind,
        location: mir::Location,
    ) -> SpannedEncodingResult<(vir::Expr, Vec<vir::Stmt>, ty::Ty<'tcx>, Option<usize>)> {
        let span = self.mir_encoder.get_span_of_location(location);
        let (encoded_place, ty, variant_idx) =
            self.mir_encoder.encode_place(place).with_span(span)?;
        trace!("encode_place(ty={:?})", ty);
        let (encoded_expr, encoding_stmts) = self
            .postprocess_place_encoding(encoded_place, encode_kind)
            .with_span(span)?;

        Ok((encoded_expr, encoding_stmts, ty, variant_idx))
    }

    fn encode_sequence_lookup_shared(
        &mut self,
        base: PlaceEncoding<'tcx>,
        index: vir::Expr,
        sequence_ty: ty::Ty<'tcx>,
    ) -> EncodingResult<(vir::Expr, Vec<vir::Stmt>)> {
        let sequence_types = self.encoder.encode_sequence_types(sequence_ty)?;

        let lookup_res: vir::Expr = self
            .cfg_method
            .add_fresh_local_var(sequence_types.elem_pred_type.clone())
            .into();
        let lookup_res_val_field = self
            .encoder
            .encode_value_expr(lookup_res.clone(), sequence_types.elem_ty_rs)?;
        let snap_lookup_res_val_field = self
            .encoder
            .patch_snapshots(vir::Expr::snap_app(lookup_res_val_field))?;

        let lookup_ret_ty = self
            .encoder
            .encode_snapshot_type(sequence_types.elem_ty_rs)?;

        let (encoded_base_expr, mut stmts) =
            self.postprocess_place_encoding(base, ArrayAccessKind::Shared)?;
        stmts.extend(self.encode_havoc_and_initialization(&lookup_res)?);

        let idx_val_int = self.encoder.patch_snapshots(vir::Expr::snap_app(index))?;

        let lookup_pure_call = sequence_types.encode_lookup_pure_call(
            self.encoder,
            encoded_base_expr.clone(),
            idx_val_int,
            lookup_ret_ty,
        );

        stmts.push(vir::Stmt::Assert(vir::Assert {
            expr: vir::Expr::predicate_access_predicate(
                sequence_types.sequence_pred_type,
                encoded_base_expr,
                vir::PermAmount::Read,
            ),
            position: vir::Position::default(),
        }));

        stmts.push(vir::Stmt::Inhale(vir::Inhale {
            expr: vir_expr! { [ lookup_pure_call ] == [ snap_lookup_res_val_field ] },
        }));
        Ok((lookup_res, stmts))
    }

    fn encode_sequence_lookup_mut(
        &mut self,
        base: PlaceEncoding<'tcx>,
        index: vir::Expr,
        sequence_ty: ty::Ty<'tcx>,
        _loan: Option<Borrow>,
        location: mir::Location,
    ) -> EncodingResult<(vir::Expr, Vec<vir::Stmt>)> {
        let sequence_types = self.encoder.encode_sequence_types(sequence_ty)?;

        let res: vir::Expr = self
            .cfg_method
            .add_fresh_local_var(sequence_types.elem_pred_type.clone())
            .into();
        let res_val_field = self
            .encoder
            .encode_value_expr(res.clone(), sequence_types.elem_ty_rs)?;
        let snap_res_val_field = self
            .encoder
            .patch_snapshots(vir::Expr::snap_app(res_val_field.clone()))?;

        let (encoded_base_expr, mut stmts) =
            self.postprocess_place_encoding(base, ArrayAccessKind::Mutable(None, location))?;

        let idx_val_int = self.encoder.patch_snapshots(vir::Expr::snap_app(index))?;

        // var res: Ref := havoc_ref()
        stmts.extend(self.encode_havoc_and_initialization(&res)?);

        // label before for old[label](..) stuff
        let before_label = self.cfg_method.get_fresh_label_name();
        stmts.push(vir::Stmt::label(&before_label));

        // exhale preconditions
        stmts.push(vir::Stmt::Assert( vir::Assert {
            expr: vir_expr!{ [idx_val_int] < [ sequence_types.len(self.encoder, encoded_base_expr.clone()) ] },
            position: vir::Position::default(),
        }));

        // exhale Array$4$i32(self)
        let array_access_pred =
            vir::Expr::pred_permission(encoded_base_expr.clone(), vir::PermAmount::Write).unwrap();

        stmts.push(vir_stmt! { exhale [array_access_pred] });

        let old = |e| vir::Expr::labelled_old(&before_label, e);
        let old_lhs = |e| vir::Expr::labelled_old("lhs", e);

        // value of res
        let lookup_ret_ty = self
            .encoder
            .encode_snapshot_type(sequence_types.elem_ty_rs)?;
        let lookup_pure_call = sequence_types.encode_lookup_pure_call(
            self.encoder,
            encoded_base_expr.clone(),
            idx_val_int.clone(),
            lookup_ret_ty.clone(),
        );
        stmts.push(vir::Stmt::Inhale(vir::Inhale {
            expr: vir_expr! { [ old(lookup_pure_call) ] == [ snap_res_val_field ] },
        }));

        // inhale magic wand
        //
        // ref$i32(result) --* Array$3$i32(self)
        //   // everything else unchanged
        //   && forall i : Int :: { Array$3$i32$pure_lookup(self, i) }
        //     0 <= i && i < 3 && index != i
        //     ==> Array$3$i32$pure_lookup(self, i)
        //       == old[lhs](Array$3$i32$pure_lookup(self, i))
        //   // the given index changed accordingly
        //   && Array$3$i32$pure_lookup(
        //     self, unfolding ... in index.val_int) == snap$i32(old[lhs](result))

        // NEEDSWORK: the vir! macro can't do everything we want here..
        // TODO: de-duplicate with encode_array_direct_assign
        let i_var: vir::Expr = vir_local! { i: Int }.into();

        let zero_le_i = vir_expr! { [ vir::Expr::from(0) ] <= [ i_var ] };
        let i_lt_len = vir_expr! { [ i_var ] < [ sequence_types.len(self.encoder, encoded_base_expr.clone()) ] };
        let i_ne_idx = vir_expr! { [ i_var ] != [ old(idx_val_int.clone()) ] };
        let idx_conditions = vir_expr! { [zero_le_i] && ([i_lt_len] && [i_ne_idx]) };
        let lookup_array_i = sequence_types.encode_lookup_pure_call(
            self.encoder,
            encoded_base_expr.clone(),
            i_var,
            lookup_ret_ty.clone(),
        );
        let lookup_same_as_old = vir_expr! { [lookup_array_i] == [old(lookup_array_i.clone())] };
        let forall_body = vir_expr! { [idx_conditions] ==> [lookup_same_as_old] };
        let all_others_unchanged =
            vir_expr! { forall i: Int :: { [lookup_array_i] } :: [ forall_body ] };
        let indexed_lookup_pure = sequence_types.encode_lookup_pure_call(
            self.encoder,
            encoded_base_expr.clone(),
            old(idx_val_int),
            lookup_ret_ty,
        );
        // TODO: old inside snapshot or the other way around?
        let snap_old_res_val_field = self
            .encoder
            .patch_snapshots(vir::Expr::snap_app(res_val_field.clone()))?;
        let indexed_updated =
            vir_expr! { [ indexed_lookup_pure ] == [ old_lhs(snap_old_res_val_field) ] };

        let magic_wand_rhs = vir_expr! { [all_others_unchanged] && [indexed_updated] };
        self.array_magic_wand_at
            .insert(location, (res_val_field, encoded_base_expr, magic_wand_rhs));

        Ok((res, stmts))
    }

    #[tracing::instrument(level = "trace", skip(self))]
    fn postprocess_place_encoding(
        &mut self,
        place_encoding: PlaceEncoding<'tcx>,
        array_encode_kind: ArrayAccessKind,
    ) -> EncodingResult<(vir::Expr, Vec<vir::Stmt>)> {
        Ok(match place_encoding {
            PlaceEncoding::Expr(e) => (e, vec![]),
            PlaceEncoding::FieldAccess { box base, field } => {
                let (expr, stmts) = self.postprocess_place_encoding(base, array_encode_kind)?;
                (expr.field(field), stmts)
            }
            PlaceEncoding::SliceAccess {
                base,
                index,
                rust_slice_ty: rust_ty,
                ..
            }
            | PlaceEncoding::ArrayAccess {
                base,
                index,
                rust_array_ty: rust_ty,
                ..
            } => {
                if let ArrayAccessKind::Mutable(loan, location) = array_encode_kind {
                    self.encode_sequence_lookup_mut(*base, index, rust_ty, loan, location)?
                } else {
                    self.encode_sequence_lookup_shared(*base, index, rust_ty)?
                }
            }
            PlaceEncoding::Variant { box base, field } => {
                let (expr, stmts) = self.postprocess_place_encoding(base, array_encode_kind)?;
                (
                    vir::Expr::Variant(vir::Variant {
                        base: Box::new(expr),
                        variant_index: field,
                        position: vir::Position::default(),
                    }),
                    stmts,
                )
            }
        })
    }

    fn register_error<T: Into<MultiSpan> + Debug>(
        &self,
        span: T,
        error_ctxt: ErrorCtxt,
    ) -> vir::Position {
        self.mir_encoder.register_error(span, error_ctxt)
    }
}

/// Whether to encode a shared or mutable array access
#[derive(Debug, PartialEq, Eq, Clone, Copy)]
enum ArrayAccessKind {
    Shared,
    Mutable(Option<Borrow>, mir::Location),
}

fn convert_loans_to_borrows(loans: &[facts::Loan]) -> Vec<Borrow> {
    loans.iter().map(|l| l.index().into()).collect()
}

/// Check if size of ProcedureContract::borrow_infos is as required
/// len: Length of borrow_infos
fn assert_one_magic_wand(len: usize) -> EncodingResult<()> {
    if len > 1 {
        Err(EncodingError::internal(format!(
            "We can have at most one magic wand in the postcondition. But we have {len:?}"
        )))
    } else {
        Ok(())
    }
}

// Checks if a type is a reference to a string, or a reference to a reference to a string, etc.
fn is_str(ty: ty::Ty<'_>) -> bool {
    match ty.kind() {
        ty::TyKind::Ref(_, inner, _) => inner.is_str() || is_str(*inner),
        _ => false,
    }
}

type PreconditionWeakening = RefinementCheckExpr;
type PostconditionStrengthening = RefinementCheckExpr;
struct RefinementCheckExpr {
    spec_functions_span: MultiSpan,
    refinement_check_expr: vir::Expr,
}
